theorem iex {x: nat} (a: wff x): $ a -> E. x a $;
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | eqcom | y = x -> x = y |
|
2 | ax_6 | E. x x = y |
|
3 | exim | A. x (x = y -> a) -> E. x x = y -> E. x a |
|
4 | 2, 3 | mpi | A. x (x = y -> a) -> E. x a |
5 | ax_12 | x = y -> a -> A. x (x = y -> a) |
|
6 | 4, 5 | syl6 | x = y -> a -> E. x a |
7 | 1, 6 | rsyl | y = x -> a -> E. x a |
8 | 7 | eex | E. y y = x -> a -> E. x a |
9 | ax_6 | E. y y = x |
|
10 | 8, 9 | ax_mp | a -> E. x a |