Theorem axrepndlem2 3739

Description: Lemma for the Axiom of Replacement with no distinct variable conditions.

Assertion

Ref	Expression
axrepndlem2	|- (((-. A.x x = y /\ -. A.x x = z) /\ -. A.y y = z) -> E.x(E.yA.z(ph -> z = y) -> A.z(z e. x <-> E.x(x e. y /\ A.yph))))

Proof of Theorem axrepndlem2

Step	Hyp	Ref	Expression
1		eq6 826	. . . . 5 |- (-. A.x x = y -> A.x -. A.x x = y)
2		eq6 826	. . . . 5 |- (-. A.x x = z -> A.x -. A.x x = z)
3	1, 2	hban 704	. . . 4 |- ((-. A.x x = y /\ -. A.x x = z) -> A.x(-. A.x x = y /\ -. A.x x = z))
4		eq6 826	. . . . . . 7 |- (-. A.x x = y -> A.y -. A.x x = y)
5		eq6 826	. . . . . . 7 |- (-. A.x x = z -> A.y -. A.x x = z)
6	4, 5	hban 704	. . . . . 6 |- ((-. A.x x = y /\ -. A.x x = z) -> A.y(-. A.x x = y /\ -. A.x x = z))
7		eq6 826	. . . . . . . 8 |- (-. A.x x = y -> A.z -. A.x x = y)
8		eq6 826	. . . . . . . 8 |- (-. A.x x = z -> A.z -. A.x x = z)
9	7, 8	hban 704	. . . . . . 7 |- ((-. A.x x = y /\ -. A.x x = z) -> A.z(-. A.x x = y /\ -. A.x x = z))
10		ax-17 925	. . . . . . . . . 10 |- (ph -> A.wph)
11	10	hbsb3 875	. . . . . . . . 9 |- ([w / x]ph -> A.x[w / x]ph)
12	11	a1i 7	. . . . . . . 8 |- ((-. A.x x = y /\ -. A.x x = z) -> ([w / x]ph -> A.x[w / x]ph))
13		ax-12 802	. . . . . . . . . 10 |- (-. A.x x = z -> (-. A.x x = y -> (z = y -> A.x z = y)))
14	13	com12 13	. . . . . . . . 9 |- (-. A.x x = y -> (-. A.x x = z -> (z = y -> A.x z = y)))
15	14	imp 277	. . . . . . . 8 |- ((-. A.x x = y /\ -. A.x x = z) -> (z = y -> A.x z = y))
16	3, 12, 15	hbimd 787	. . . . . . 7 |- ((-. A.x x = y /\ -. A.x x = z) -> (([w / x]ph -> z = y) -> A.x([w / x]ph -> z = y)))
17	9, 16	hbald 790	. . . . . 6 |- ((-. A.x x = y /\ -. A.x x = z) -> (A.z([w / x]ph -> z = y) -> A.xA.z([w / x]ph -> z = y)))
18	6, 17	hbexd 791	. . . . 5 |- ((-. A.x x = y /\ -. A.x x = z) -> (E.yA.z([w / x]ph -> z = y) -> A.xE.yA.z([w / x]ph -> z = y)))
19		ddeel1 1003	. . . . . . . 8 |- (-. A.x x = z -> (z e. w -> A.x z e. w))
20	19	adantl 305	. . . . . . 7 |- ((-. A.x x = y /\ -. A.x x = z) -> (z e. w -> A.x z e. w))
21		ax-17 925	. . . . . . . 8 |- ((-. A.x x = y /\ -. A.x x = z) -> A.w(-. A.x x = y /\ -. A.x x = z))
22		ddeel2 1004	. . . . . . . . . 10 |- (-. A.x x = y -> (w e. y -> A.x w e. y))
23	22	adantr 306	. . . . . . . . 9 |- ((-. A.x x = y /\ -. A.x x = z) -> (w e. y -> A.x w e. y))
24	6, 12	hbald 790	. . . . . . . . 9 |- ((-. A.x x = y /\ -. A.x x = z) -> (A.y[w / x]ph -> A.xA.y[w / x]ph))
25	23, 24	hband 788	. . . . . . . 8 |- ((-. A.x x = y /\ -. A.x x = z) -> ((w e. y /\ A.y[w / x]ph) -> A.x(w e. y /\ A.y[w / x]ph)))
26	21, 25	hbexd 791	. . . . . . 7 |- ((-. A.x x = y /\ -. A.x x = z) -> (E.w(w e. y /\ A.y[w / x]ph) -> A.xE.w(w e. y /\ A.y[w / x]ph)))
27	3, 20, 26	hbbid 789	. . . . . 6 |- ((-. A.x x = y /\ -. A.x x = z) -> ((z e. w <-> E.w(w e. y /\ A.y[w / x]ph)) -> A.x(z e. w <-> E.w(w e. y /\ A.y[w / x]ph))))
28	9, 27	hbald 790	. . . . 5 |- ((-. A.x x = y /\ -. A.x x = z) -> (A.z(z e. w <-> E.w(w e. y /\ A.y[w / x]ph)) -> A.xA.z(z e. w <-> E.w(w e. y /\ A.y[w / x]ph))))
29	3, 18, 28	hbimd 787	. . . 4 |- ((-. A.x x = y /\ -. A.x x = z) -> ((E.yA.z([w / x]ph -> z = y) -> A.z(z e. w <-> E.w(w e. y /\ A.y[w / x]ph))) -> A.x(E.yA.z([w / x]ph -> z = y) -> A.z(z e. w <-> E.w(w e. y /\ A.y[w / x]ph)))))
30		nd5 3736	. . . . . . . . 9 |- (-. A.x x = y -> (w = x -> A.y w = x))
31	30	adantr 306	. . . . . . . 8 |- ((-. A.x x = y /\ -. A.x x = z) -> (w = x -> A.y w = x))
32	31	imdistani 340	. . . . . . 7 |- (((-. A.x x = y /\ -. A.x x = z) /\ w = x) -> ((-. A.x x = y /\ -. A.x x = z) /\ A.y w = x))
33		hba1 698	. . . . . . . . 9 |- (A.y w = x -> A.yA.y w = x)
34	6, 33	hban 704	. . . . . . . 8 |- (((-. A.x x = y /\ -. A.x x = z) /\ A.y w = x) -> A.y((-. A.x x = y /\ -. A.x x = z) /\ A.y w = x))
35		nd5 3736	. . . . . . . . . . 11 |- (-. A.x x = z -> (w = x -> A.z w = x))
36	35	imdistani 340	. . . . . . . . . 10 |- ((-. A.x x = z /\ w = x) -> (-. A.x x = z /\ A.z w = x))
37		hba1 698	. . . . . . . . . . . 12 |- (A.z w = x -> A.zA.z w = x)
38	8, 37	hban 704	. . . . . . . . . . 11 |- ((-. A.x x = z /\ A.z w = x) -> A.z(-. A.x x = z /\ A.z w = x))
39		sbequ12r 866	. . . . . . . . . . . . . 14 |- (w = x -> ([w / x]ph <-> ph))
40	39	imbi1d 465	. . . . . . . . . . . . 13 |- (w = x -> (([w / x]ph -> z = y) <-> (ph -> z = y)))
41	40	a4s 682	. . . . . . . . . . . 12 |- (A.z w = x -> (([w / x]ph -> z = y) <-> (ph -> z = y)))
42	41	adantl 305	. . . . . . . . . . 11 |- ((-. A.x x = z /\ A.z w = x) -> (([w / x]ph -> z = y) <-> (ph -> z = y)))
43	38, 42	biald 782	. . . . . . . . . 10 |- ((-. A.x x = z /\ A.z w = x) -> (A.z([w / x]ph -> z = y) <-> A.z(ph -> z = y)))
44	36, 43	syl 12	. . . . . . . . 9 |- ((-. A.x x = z /\ w = x) -> (A.z([w / x]ph -> z = y) <-> A.z(ph -> z = y)))
45		pm3.27 260	. . . . . . . . 9 |- ((-. A.x x = y /\ -. A.x x = z) -> -. A.x x = z)
46		ax-4 673	. . . . . . . . 9 |- (A.y w = x -> w = x)
47	44, 45, 46	syl2an 349	. . . . . . . 8 |- (((-. A.x x = y /\ -. A.x x = z) /\ A.y w = x) -> (A.z([w / x]ph -> z = y) <-> A.z(ph -> z = y)))
48	34, 47	biexd 783	. . . . . . 7 |- (((-. A.x x = y /\ -. A.x x = z) /\ A.y w = x) -> (E.yA.z([w / x]ph -> z = y) <-> E.yA.z(ph -> z = y)))
49	32, 48	syl 12	. . . . . 6 |- (((-. A.x x = y /\ -. A.x x = z) /\ w = x) -> (E.yA.z([w / x]ph -> z = y) <-> E.yA.z(ph -> z = y)))
50	35	adantl 305	. . . . . . . 8 |- ((-. A.x x = y /\ -. A.x x = z) -> (w = x -> A.z w = x))
51	50	imdistani 340	. . . . . . 7 |- (((-. A.x x = y /\ -. A.x x = z) /\ w = x) -> ((-. A.x x = y /\ -. A.x x = z) /\ A.z w = x))
52	9, 37	hban 704	. . . . . . . 8 |- (((-. A.x x = y /\ -. A.x x = z) /\ A.z w = x) -> A.z((-. A.x x = y /\ -. A.x x = z) /\ A.z w = x))
53		a14b 820	. . . . . . . . . . 11 |- (w = x -> (z e. w <-> z e. x))
54	53	adantl 305	. . . . . . . . . 10 |- (((-. A.x x = y /\ -. A.x x = z) /\ w = x) -> (z e. w <-> z e. x))
55		a13b 819	. . . . . . . . . . . . . . 15 |- (w = x -> (w e. y <-> x e. y))
56	55	adantl 305	. . . . . . . . . . . . . 14 |- (((-. A.x x = y /\ -. A.x x = z) /\ w = x) -> (w e. y <-> x e. y))
57		sbal2 1005	. . . . . . . . . . . . . . . . . 18 |- (-. A.y y = x -> ([w / x]A.yph <-> A.y[w / x]ph))
58	57	eq4ds 823	. . . . . . . . . . . . . . . . 17 |- (-. A.x x = y -> ([w / x]A.