Theorem subsnex ≪ | index | src | ≫ 

theorem subsnex (A: set) {a x: nat}:
  $ subsn A <-> E. a A. x (x e. A -> x = a) $;
StepHypRefExpression
1 biidd 
a = the A -> (x e. A <-> x e. A)
2 eqidd 
a = the A -> x = x
3 id 
a = the A -> a = the A
4 2, 3 eqeqd 
a = the A -> (x = a <-> x = the A)
5 1, 4 imeqd 
a = the A -> (x e. A -> x = a <-> x e. A -> x = the A)
6 5 aleqd 
a = the A -> (A. x (x e. A -> x = a) <-> A. x (x e. A -> x = the A))
7 6 iexe 
A. x (x e. A -> x = the A) -> E. a A. x (x e. A -> x = a)
8 eqcom 
the A = x -> x = the A
9 subsnthe 
subsn A -> x e. A -> the A = x
10 8, 9 syl6 
subsn A -> x e. A -> x = the A
11 10 iald 
subsn A -> A. x (x e. A -> x = the A)
12 7, 11 syl 
subsn A -> E. a A. x (x e. A -> x = a)
13 id 
x = a1 -> x = a1
14 eqsidd 
x = a1 -> A == A
15 13, 14 eleqd 
x = a1 -> (x e. A <-> a1 e. A)
16 eqidd 
x = a1 -> a = a
17 13, 16 eqeqd 
x = a1 -> (x = a <-> a1 = a)
18 15, 17 imeqd 
x = a1 -> (x e. A -> x = a <-> a1 e. A -> a1 = a)
19 18 eale 
A. x (x e. A -> x = a) -> a1 e. A -> a1 = a
20 19 eqsubsnd 
A. x (x e. A -> x = a) -> subsn A
21 20 eex 
E. a A. x (x e. A -> x = a) -> subsn A
22 12, 21 ibii 
subsn A <-> E. a A. x (x e. A -> x = a)

Axiom use

axs_prop_calc (ax_1, ax_2, ax_3, ax_mp, itru), axs_pred_calc (ax_gen, ax_4, ax_5, ax_6, ax_7, ax_10, ax_11, ax_12), axs_set (elab, ax_8), axs_the (theid)