theorem exbi (a: wff) {x: nat}: $ E. x a <-> a $;
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | con1b | (~a <-> A. x ~a) -> (~A. x ~a <-> a) |
|
2 | 1 | conv ex | (~a <-> A. x ~a) -> (E. x a <-> a) |
3 | bicom | (A. x ~a <-> ~a) -> (~a <-> A. x ~a) |
|
4 | albi | A. x ~a <-> ~a |
|
5 | 3, 4 | ax_mp | ~a <-> A. x ~a |
6 | 2, 5 | ax_mp | E. x a <-> a |