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 $;

Step	Hyp	Ref	Expression
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	2	bitr3*	(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	5	eleq1*	fst a, snd a e. S\ x, B <-> a e. S\ x, B
7	2, 6	bitr3*	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)