Theorem iex | index | src |

theorem iex {x: nat} (a: wff x): $ a -> E. x a $;
StepHypRefExpression
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

Axiom use

axs_prop_calc (ax_1, ax_2, ax_3, ax_mp), axs_pred_calc (ax_gen, ax_4, ax_5, ax_6, ax_7, ax_12)