Theorem sabxab ≪ | index | src | ≫ 

theorem sabxab (A: set) (G: wff) {x y: nat} (B: set x):
  $ G -> y e. B -> x e. A $ >
  $ G -> S\ x, B == X\ x e. A, B $;
StepHypRefExpression
1 elsabs 
z, y e. S\ x, B <-> y e. S[z / x] B
2 elxabs 
z, y e. X\ x e. A, B <-> z e. A /\ y e. S[z / x] B
3 bian1a 
(y e. S[z / x] B -> z e. A) -> (z e. A /\ y e. S[z / x] B <-> y e. S[z / x] B)
4 nfv 
F/ x G
5 nfsbs1 
FS/ x S[z / x] B
6 5 nfel2 
F/ x y e. S[z / x] B
7 nfv 
F/ x z e. A
8 6, 7 nfim 
F/ x y e. S[z / x] B -> z e. A
9 4, 8 nfim 
F/ x G -> y e. S[z / x] B -> z e. A
10 hyp h 
G -> y e. B -> x e. A
11 sbsq 
x = z -> B == S[z / x] B
12 11 eleq2d 
x = z -> (y e. B <-> y e. S[z / x] B)
13 eleq1 
x = z -> (x e. A <-> z e. A)
14 12, 13 imeqd 
x = z -> (y e. B -> x e. A <-> y e. S[z / x] B -> z e. A)
15 14 imeq2d 
x = z -> (G -> y e. B -> x e. A <-> G -> y e. S[z / x] B -> z e. A)
16 9, 10, 15 sbethh 
G -> y e. S[z / x] B -> z e. A
17 3, 16 syl 
G -> (z e. A /\ y e. S[z / x] B <-> y e. S[z / x] B)
18 17 bicomd 
G -> (y e. S[z / x] B <-> z e. A /\ y e. S[z / x] B)
19 1, 2, 18 bitr4g 
G -> (z, y e. S\ x, B <-> z, y e. X\ x e. A, B)
20 19 eqrd2 
G -> S\ x, B == X\ x e. A, B

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, the0), axs_peano (peano1, peano2, peano5, addeq, muleq, add0, addS, mul0, mulS)