Theorem axrepndlem2 4917

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		hbnae 1143	. . . . 5 |- (-. A.x x = y -> A.x -. A.x x = y)
2		hbnae 1143	. . . . 5 |- (-. A.x x = z -> A.x -. A.x x = z)
3	1, 2	hban 1006	. . . 4 |- ((-. A.x x = y /\ -. A.x x = z) -> A.x(-. A.x x = y /\ -. A.x x = z))
4		hbnae 1143	. . . . . . 7 |- (-. A.x x = y -> A.y -. A.x x = y)
5		hbnae 1143	. . . . . . 7 |- (-. A.x x = z -> A.y -. A.x x = z)
6	4, 5	hban 1006	. . . . . 6 |- ((-. A.x x = y /\ -. A.x x = z) -> A.y(-. A.x x = y /\ -. A.x x = z))
7		hbnae 1143	. . . . . . . 8 |- (-. A.x x = y -> A.z -. A.x x = y)
8		hbnae 1143	. . . . . . . 8 |- (-. A.x x = z -> A.z -. A.x x = z)
9	7, 8	hban 1006	. . . . . . 7 |- ((-. A.x x = y /\ -. A.x x = z) -> A.z(-. A.x x = y /\ -. A.x x = z))
10		ax-17 968	. . . . . . . . . 10 |- (ph -> A.wph)
11	10	hbsb3 1202	. . . . . . . . 9 |- ([w / x]ph -> A.x[w / x]ph)
12	11	a1i 8	. . . . . . . 8 |- ((-. A.x x = y /\ -. A.x x = z) -> ([w / x]ph -> A.x[w / x]ph))
13		ax-12 965	. . . . . . . . 9 |- (-. A.x x = z -> (-. A.x x = y -> (z = y -> A.x z = y)))
14	13	impcom 351	. . . . . . . 8 |- ((-. A.x x = y /\ -. A.x x = z) -> (z = y -> A.x z = y))
15	3, 12, 14	hbimd 1106	. . . . . . 7 |- ((-. A.x x = y /\ -. A.x x = z) -> (([w / x]ph -> z = y) -> A.x([w / x]ph -> z = y)))
16	9, 15	hbald 1109	. . . . . 6 |- ((-. A.x x = y /\ -. A.x x = z) -> (A.z([w / x]ph -> z = y) -> A.xA.z([w / x]ph -> z = y)))
17	6, 16	hbexd 1110	. . . . 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)))
18		dveel1 1349	. . . . . . . 8 |- (-. A.x x = z -> (z e. w -> A.x z e. w))
19	18	adantl 388	. . . . . . 7 |- ((-. A.x x = y /\ -. A.x x = z) -> (z e. w -> A.x z e. w))
20		ax-17 968	. . . . . . . 8 |- ((-. A.x x = y /\ -. A.x x = z) -> A.w(-. A.x x = y /\ -. A.x x = z))
21		dveel2 1350	. . . . . . . . . 10 |- (-. A.x x = y -> (w e. y -> A.x w e. y))
22	21	adantr 389	. . . . . . . . 9 |- ((-. A.x x = y /\ -. A.x x = z) -> (w e. y -> A.x w e. y))
23	6, 12	hbald 1109	. . . . . . . . 9 |- ((-. A.x x = y /\ -. A.x x = z) -> (A.y[w / x]ph -> A.xA.y[w / x]ph))
24	22, 23	hband 1107	. . . . . . . 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)))
25	20, 24	hbexd 1110	. . . . . . 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)))
26	3, 19, 25	hbbid 1108	. . . . . 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))))
27	9, 26	hbald 1109	. . . . 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))))
28	3, 17, 27	hbimd 1106	. . . 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)))))
29		nd5 4914	. . . . . . . . 9 |- (-. A.x x = y -> (w = x -> A.y w = x))
30	29	adantr 389	. . . . . . . 8 |- ((-. A.x x = y /\ -. A.x x = z) -> (w = x -> A.y w = x))
31	30	imdistani 443	. . . . . . 7 |- (((-. A.x x = y /\ -. A.x x = z) /\ w = x) -> ((-. A.x x = y /\ -. A.x x = z) /\ A.y w = x))
32		hba1 1000	. . . . . . . . 9 |- (A.y w = x -> A.yA.y w = x)
33	6, 32	hban 1006	. . . . . . . 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))
34		nd5 4914	. . . . . . . . . . 11 |- (-. A.x x = z -> (w = x -> A.z w = x))
35	34	imdistani 443	. . . . . . . . . 10 |- ((-. A.x x = z /\ w = x) -> (-. A.x x = z /\ A.z w = x))
36		hba1 1000	. . . . . . . . . . . 12 |- (A.z w = x -> A.zA.z w = x)
37	8, 36	hban 1006	. . . . . . . . . . 11 |- ((-. A.x x = z /\ A.z w = x) -> A.z(-. A.x x = z /\ A.z w = x))
38		sbequ12r 1178	. . . . . . . . . . . . . 14 |- (w = x -> ([w / x]ph <-> ph))
39	38	imbi1d 611	. . . . . . . . . . . . 13 |- (w = x -> (([w / x]ph -> z = y) <-> (ph -> z = y)))
40	39	a4s 981	. . . . . . . . . . . 12 |- (A.z w = x -> (([w / x]ph -> z = y) <-> (ph -> z = y)))
41	40	adantl 388	. . . . . . . . . . 11 |- ((-. A.x x = z /\ A.z w = x) -> (([w / x]ph -> z = y) <-> (ph -> z = y)))
42	37, 41	albid 1100	. . . . . . . . . 10 |- ((-. A.x x = z /\ A.z w = x) -> (A.z([w / x]ph -> z = y) <-> A.z(ph -> z = y)))
43	35, 42	syl 10	. . . . . . . . 9 |- ((-. A.x x = z /\ w = x) -> (A.z([w / x]ph -> z = y) <-> A.z(ph -> z = y)))
44		pm3.27 323	. . . . . . . . 9 |- ((-. A.x x = y /\ -. A.x x = z) -> -. A.x x = z)
45		ax-4 970	. . . . . . . . 9 |- (A.y w = x -> w = x)
46	43, 44, 45	syl2an 454	. . . . . . . 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)))
47	33, 46	exbid 1101	. . . . . . 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)))
48	31, 47	syl 10	. . . . . 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)))
49	34	adantl 388	. . . . . . . 8 |- ((-. A.x x = y /\ -. A.x x = z) -> (w = x -> A.z w = x))
50	49	imdistani 443	. . . . . . 7 |- (((-. A.x x = y /\ -. A.x x = z) /\ w = x) -> ((-. A.x x = y /\ -. A.x x = z) /\ A.z w = x))
51	9, 36	hban 1006	. . . . . . . 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))
52		elequ2 1133	. . . . . . . . . . 11 |- (w = x -> (z e. w <-> z e. x))
53	52	adantl 388	. . . . . . . . . 10 |- (((-. A.x x = y /\ -. A.x x = z) /\ w = x) -> (z e. w <-> z e. x))
54		elequ1 1132	. . . . . . . . . . . . . . 15 |- (w = x -> (w e. y <-> x e. y))
55	54	adantl 388	. . . . . . . . . . . . . 14 |- (((-. A.x x = y /\ -. A.x x = z) /\ w = x) -> (w e. y <-> x e. y))
56		sbal2 1351	. . . . . . . . . . . . . . . . . 18 |- (-. A.y y =