theorem abid {x: nat} (p: wff x): $ x e. {x | p} <-> p $;
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | bitr | (x e. {x | p} <-> [x / x] p) -> ([x / x] p <-> p) -> (x e. {x | p} <-> p) |
|
2 | elab2 | x e. {x | p} <-> [x / x] p |
|
3 | 1, 2 | ax_mp | ([x / x] p <-> p) -> (x e. {x | p} <-> p) |
4 | sbid | [x / x] p <-> p |
|
5 | 3, 4 | ax_mp | x e. {x | p} <-> p |