Theorem elxabs ≪ | index | src | ≫ 

theorem elxabs (A: set) (a b: nat) {x: nat} (B: set x):
  $ a, b e. X\ x e. A, B <-> a e. A /\ b e. S[a / x] B $;
StepHypRefExpression
1 fstpr 
fst (a, b) = a
2 fsteq 
p = a, b -> fst p = fst (a, b)
3 1, 2 syl6eq 
p = a, b -> fst p = a
4 3 eleq1d 
p = a, b -> (fst p e. A <-> a e. A)
5 sndpr 
snd (a, b) = b
6 sndeq 
p = a, b -> snd p = snd (a, b)
7 5, 6 syl6eq 
p = a, b -> snd p = b
8 3 sbseq1d 
p = a, b -> S[fst p / x] B == S[a / x] B
9 7, 8 eleqd 
p = a, b -> (snd p e. S[fst p / x] B <-> b e. S[a / x] B)
10 4, 9 aneqd 
p = a, b -> (fst p e. A /\ snd p e. S[fst p / x] B <-> a e. A /\ b e. S[a / x] B)
11 10 elabe 
a, b e. {p | fst p e. A /\ snd p e. S[fst p / x] B} <-> a e. A /\ b e. S[a / x] B
12 11 conv xab 
a, b e. X\ x e. A, B <-> a e. A /\ b e. S[a / x] 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)