Theorem eexsabd ≪ | index | src | ≫

theorem eexsabd (G p: wff) {x z: nat} (y: nat x z) (A: set x):
  $ G -> z e. A -> p $ >
  $ G -> y e. S\ x, A -> p $;

Step	Hyp	Ref	Expression
1		eleq1	w = y -> (w e. S\ x, A <-> y e. S\ x, A)
2	1	iexe	y e. S\ x, A -> E. w w e. S\ x, A
3		eleq1	fst w, snd w = w -> (fst w, snd w e. S\ x, A <-> w e. S\ x, A)
4		fstsnd	fst w, snd w = w
5	3, 4	ax_mp	fst w, snd w e. S\ x, A <-> w e. S\ x, A
6		elsabs	fst w, snd w e. S\ x, A <-> snd w e. S[fst w / x] A
7		eleq1	z = snd w -> (z e. S[fst w / x] A <-> snd w e. S[fst w / x] A)
8	7	iexe	snd w e. S[fst w / x] A -> E. z z e. S[fst w / x] A
9		nfv	F/ x G
10		nfsbs1	FS/ x S[fst w / x] A
11	10	nfel2	F/ x z e. S[fst w / x] A
12		nfv	F/ x p
13	11, 12	nfim	F/ x z e. S[fst w / x] A -> p
14	9, 13	nfim	F/ x G -> z e. S[fst w / x] A -> p
15		hyp h	G -> z e. A -> p
16		sbsq	x = fst w -> A == S[fst w / x] A
17	16	eleq2d	x = fst w -> (z e. A <-> z e. S[fst w / x] A)
18	17	imeq1d	x = fst w -> (z e. A -> p <-> z e. S[fst w / x] A -> p)
19	18	imeq2d	x = fst w -> (G -> z e. A -> p <-> G -> z e. S[fst w / x] A -> p)
20	14, 15, 19	sbethh	G -> z e. S[fst w / x] A -> p
21	20	eexd	G -> E. z z e. S[fst w / x] A -> p
22	8, 21	syl5	G -> snd w e. S[fst w / x] A -> p
23	6, 22	syl5bi	G -> fst w, snd w e. S\ x, A -> p
24	5, 23	syl5bir	G -> w e. S\ x, A -> p
25	24	eexd	G -> E. w w e. S\ x, A -> p
26	2, 25	syl5	G -> y e. S\ x, A -> p

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)