Theorem sabssxped ≪ | index | src | ≫ 

theorem sabssxped (A C: set) (G: wff) (a: nat) (p: wff) {x: nat} (B: set x):
  $ G /\ x = fst a -> snd a e. B -> p /\ x e. A /\ snd a e. C $ >
  $ G -> a e. S\ x, B -> p /\ a e. Xp A C $;
StepHypRefExpression
1 bitr3 
(fst a, snd a e. S\ x, B <-> snd a e. S[fst a / x] B) -> (fst a, snd a e. S\ x, B <-> a e. S\ x, B) -> (snd a e. S[fst a / x] B <-> a e. S\ x, B)
2 elsabs 
fst a, snd a e. S\ x, B <-> snd a e. S[fst a / x] B
3 1, 2 ax_mp 
(fst a, snd a e. S\ x, B <-> a e. S\ x, B) -> (snd a e. S[fst a / x] B <-> a e. S\ x, B)
4 eleq1 
fst a, snd a = a -> (fst a, snd a e. S\ x, B <-> a e. S\ x, B)
5 fstsnd 
fst a, snd a = a
6 4, 5 ax_mp 
fst a, snd a e. S\ x, B <-> a e. S\ x, B
7 3, 6 ax_mp 
snd a e. S[fst a / x] B <-> a e. S\ x, B
8 elxp 
a e. Xp A C <-> fst a e. A /\ snd a e. C
9 8 aneq2i 
p /\ a e. Xp A C <-> p /\ (fst a e. A /\ snd a e. C)
10 ax_6 
E. x x = fst a
11 nfv 
F/ x G
12 nfsbs1 
FS/ x S[fst a / x] B
13 12 nfel2 
F/ x snd a e. S[fst a / x] B
14 nfv 
F/ x p /\ (fst a e. A /\ snd a e. C)
15 13, 14 nfim 
F/ x snd a e. S[fst a / x] B -> p /\ (fst a e. A /\ snd a e. C)
16 sbsq 
x = fst a -> B == S[fst a / x] B
17 16 eleq2d 
x = fst a -> (snd a e. B <-> snd a e. S[fst a / x] B)
18 anass 
p /\ fst a e. A /\ snd a e. C <-> p /\ (fst a e. A /\ snd a e. C)
19 eleq1 
x = fst a -> (x e. A <-> fst a e. A)
20 19 aneq2d 
x = fst a -> (p /\ x e. A <-> p /\ fst a e. A)
21 20 aneq1d 
x = fst a -> (p /\ x e. A /\ snd a e. C <-> p /\ fst a e. A /\ snd a e. C)
22 18, 21 syl6bb 
x = fst a -> (p /\ x e. A /\ snd a e. C <-> p /\ (fst a e. A /\ snd a e. C))
23 17, 22 imeqd 
x = fst a -> (snd a e. B -> p /\ x e. A /\ snd a e. C <-> snd a e. S[fst a / x] B -> p /\ (fst a e. A /\ snd a e. C))
24 23 anwr 
G /\ x = fst a -> (snd a e. B -> p /\ x e. A /\ snd a e. C <-> snd a e. S[fst a / x] B -> p /\ (fst a e. A /\ snd a e. C))
25 hyp h 
G /\ x = fst a -> snd a e. B -> p /\ x e. A /\ snd a e. C
26 24, 25 mpbid 
G /\ x = fst a -> snd a e. S[fst a / x] B -> p /\ (fst a e. A /\ snd a e. C)
27 26 exp 
G -> x = fst a -> snd a e. S[fst a / x] B -> p /\ (fst a e. A /\ snd a e. C)
28 11, 15, 27 eexdh 
G -> E. x x = fst a -> snd a e. S[fst a / x] B -> p /\ (fst a e. A /\ snd a e. C)
29 10, 28 mpi 
G -> snd a e. S[fst a / x] B -> p /\ (fst a e. A /\ snd a e. C)
30 9, 29 syl6ibr 
G -> snd a e. S[fst a / x] B -> p /\ a e. Xp A C
31 7, 30 syl5bir 
G -> a e. S\ x, B -> p /\ a e. Xp A C

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)