theorem eexb {x: nat} (a: wff x) (b: wff): $ E. x a -> b <-> A. x (a -> b) $;
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | nfex1 | F/ x E. x a |
|
2 | nfv | F/ x b |
|
3 | 1, 2 | nfim | F/ x E. x a -> b |
4 | iex | a -> E. x a |
|
5 | 4 | imim1i | (E. x a -> b) -> a -> b |
6 | 3, 5 | ialdh | (E. x a -> b) -> A. x (a -> b) |
7 | nfal1 | F/ x A. x (a -> b) |
|
8 | eal | A. x (a -> b) -> a -> b |
|
9 | 7, 2, 8 | eexdh | A. x (a -> b) -> E. x a -> b |
10 | 6, 9 | ibii | E. x a -> b <-> A. x (a -> b) |