Theorem axrepnd 4869

Description: A version of the Axiom of Replacement with no distinct variable conditions.

Assertion

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

Proof of Theorem axrepnd

Step	Hyp	Ref	Expression
1		axrepndlem2 4868	. . . 4 |- (((-. 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))))
2		hbnae 1130	. . . . . . 7 |- (-. A.x x = y -> A.x -. A.x x = y)
3		hbnae 1130	. . . . . . 7 |- (-. A.x x = z -> A.x -. A.x x = z)
4	2, 3	hban 985	. . . . . 6 |- ((-. A.x x = y /\ -. A.x x = z) -> A.x(-. A.x x = y /\ -. A.x x = z))
5		hbnae 1130	. . . . . 6 |- (-. A.y y = z -> A.x -. A.y y = z)
6	4, 5	hban 985	. . . . 5 |- (((-. A.x x = y /\ -. A.x x = z) /\ -. A.y y = z) -> A.x((-. A.x x = y /\ -. A.x x = z) /\ -. A.y y = z))
7		hbnae 1130	. . . . . . . . 9 |- (-. A.x x = y -> A.z -. A.x x = y)
8		hbnae 1130	. . . . . . . . 9 |- (-. A.x x = z -> A.z -. A.x x = z)
9	7, 8	hban 985	. . . . . . . 8 |- ((-. A.x x = y /\ -. A.x x = z) -> A.z(-. A.x x = y /\ -. A.x x = z))
10		hbnae 1130	. . . . . . . 8 |- (-. A.y y = z -> A.z -. A.y y = z)
11	9, 10	hban 985	. . . . . . 7 |- (((-. A.x x = y /\ -. A.x x = z) /\ -. A.y y = z) -> A.z((-. A.x x = y /\ -. A.x x = z) /\ -. A.y y = z))
12		ax15 1339	. . . . . . . . . . . . 13 |- (-. A.y y = z -> (-. A.y y = x -> (z e. x -> A.y z e. x)))
13	12	com12 11	. . . . . . . . . . . 12 |- (-. A.y y = x -> (-. A.y y = z -> (z e. x -> A.y z e. x)))
14	13	nalequcoms 1127	. . . . . . . . . . 11 |- (-. A.x x = y -> (-. A.y y = z -> (z e. x -> A.y z e. x)))
15	14	imp 350	. . . . . . . . . 10 |- ((-. A.x x = y /\ -. A.y y = z) -> (z e. x -> A.y z e. x))
16	15	adantlr 393	. . . . . . . . 9 |- (((-. A.x x = y /\ -. A.x x = z) /\ -. A.y y = z) -> (z e. x -> A.y z e. x))
17		ax-4 951	. . . . . . . . 9 |- (A.y z e. x -> z e. x)
18	16, 17	impbid1 515	. . . . . . . 8 |- (((-. A.x x = y /\ -. A.x x = z) /\ -. A.y y = z) -> (z e. x <-> A.y z e. x))
19		ax15 1339	. . . . . . . . . . . . . 14 |- (-. A.z z = x -> (-. A.z z = y -> (x e. y -> A.z x e. y)))
20	19	imp 350	. . . . . . . . . . . . 13 |- ((-. A.z z = x /\ -. A.z z = y) -> (x e. y -> A.z x e. y))
21		alequcom 1125	. . . . . . . . . . . . . 14 |- (A.z z = x -> A.x x = z)
22	21	con3i 98	. . . . . . . . . . . . 13 |- (-. A.x x = z -> -. A.z z = x)
23		alequcom 1125	. . . . . . . . . . . . . 14 |- (A.z z = y -> A.y y = z)
24	23	con3i 98	. . . . . . . . . . . . 13 |- (-. A.y y = z -> -. A.z z = y)
25	20, 22, 24	syl2an 454	. . . . . . . . . . . 12 |- ((-. A.x x = z /\ -. A.y y = z) -> (x e. y -> A.z x e. y))
26	25	adantll 392	. . . . . . . . . . 11 |- (((-. A.x x = y /\ -. A.x x = z) /\ -. A.y y = z) -> (x e. y -> A.z x e. y))
27		ax-4 951	. . . . . . . . . . 11 |- (A.z x e. y -> x e. y)
28	26, 27	impbid1 515	. . . . . . . . . 10 |- (((-. A.x x = y /\ -. A.x x = z) /\ -. A.y y = z) -> (x e. y <-> A.z x e. y))
29	28	anbi1d 615	. . . . . . . . 9 |- (((-. A.x x = y /\ -. A.x x = z) /\ -. A.y y = z) -> ((x e. y /\ A.yph) <-> (A.z x e. y /\ A.yph)))
30	6, 29	exbid 1081	. . . . . . . 8 |- (((-. A.x x = y /\ -. A.x x = z) /\ -. A.y y = z) -> (E.x(x e. y /\ A.yph) <-> E.x(A.z x e. y /\ A.yph)))
31	18, 30	bibi12d 627	. . . . . . 7 |- (((-. A.x x = y /\ -. A.x x = z) /\ -. A.y y = z) -> ((z e. x <-> E.x(x e. y /\ A.yph)) <-> (A.y z e. x <-> E.x(A.z x e. y /\ A.yph))))
32	11, 31	albid 1080	. . . . . 6 |- (((-. A.x x = y /\ -. A.x x = z) /\ -. A.y y = z) -> (A.z(z e. x <-> E.x(x e. y /\ A.yph)) <-> A.z(A.y z e. x <-> E.x(A.z x e. y /\ A.yph))))
33	32	imbi2d 610	. . . . 5 |- (((-. A.x x = y /\ -. A.x x = z) /\ -. A.y y = z) -> ((E.yA.z(ph -> z = y) -> A.z(z e. x <-> E.x(x e. y /\ A.yph))) <-> (E.yA.z(ph -> z = y) -> A.z(A.y z e. x <-> E.x(A.z x e. y /\ A.yph)))))
34	6, 33	exbid 1081	. . . 4 |- (((-. 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))) <-> E.x(E.yA.z(ph -> z = y) -> A.z(A.y z e. x <-> E.x(A.z x e. y /\ A.yph)))))
35	1, 34	mpbid 195	. . 3 |- (((-. A.x x = y /\ -. A.x x = z) /\ -. A.y y = z) -> E.x(E.yA.z(ph -> z = y) -> A.z(A.y z e. x <-> E.x(A.z x e. y /\ A.yph))))
36	35	exp31 376	. 2 |- (-. A.x x = y -> (-. A.x x = z -> (-. A.y y = z -> E.x(E.yA.z(ph -> z = y) -> A.z(A.y z e. x <-> E.x(A.z x e. y /\ A.yph))))))
37		hbae 1128	. . . . 5 |- (A.x x = y -> A.zA.x x = y)
38		pm5.21 674	. . . . . 6 |- ((-. A.y z e. x /\ -. E.x(A.z x e. y /\ A.yph)) -> (A.y z e. x <-> E.x(A.z x e. y /\ A.yph)))
39		nd2 4862	. . . . . . 7 |- (A.y y = x -> -. A.y z e. x)
40	39	alequcoms 1126	. . . . . 6 |- (A.x x = y -> -. A.y z e. x)
41		hbae 1128	. . . . . . 7 |- (A.x x = y -> A.xA.x x = y)
42		nd3 4863	. . . . . . . 8 |- (A.x x = y -> -. A.z x e. y)
43	42	intnanrd 691	. . . . . . 7 |- (A.x x = y -> -. (A.z x e. y /\ A.yph))
44	41, 43	nexd 1078	. . . . . 6 |- (A.x x = y -> -. E.x(A.z x e. y /\ A.yph))
45	38, 40, 44	sylanc 471	. . . . 5 |- (A.x x = y -> (A.y z e. x <-> E.x(A.z x e. y /\ A.yph)))
46	37, 45	19.21ai 974	. . . 4 |- (A.x x = y -> A.z(A.y z e. x <-> E.x(A.z x e. y /\ A.yph)))
47	46	a1d 12	. . 3 |- (A.x x = y -> (E.yA.z(ph -> z = y) -> A.z(A.y z e. x <-> E.x(A.z x e. y /\ A.yph))))
48		19.8a 1005	. . 3 |- ((E.yA.z(ph -> z = y) -> A.z(A.y z e. x <-> E.x(A.z x e. y /\ A.yph))) -> E.x(E.yA.z(ph -> z = y) -> A.z(A.y z e. x <-> E.x(A.z x e. y /\ A.yph))))
49	47, 48	syl 10	. 2 |- (A.x x = y -> E.x(E.yA.z(ph -> z = y) -> A.z(A.y z e. x <-> E.x(A.z x e. y /\ A.yph))))
50		hbae 1128	. . . . 5 |- (A.x x = z -> A.zA.x x = z)
51		nd4 4864	. . . . . 6 |- (A.x x = z -> -. A.y z e. x)
52		hbae 1128	. . . . . . 7 |- (A.x x = z -> A.xA.x x = z)
53		nd1 4861	. . . . . . . . 9 |- (A.z z = x -> -. A.z x e. y)
54	53	alequcoms 1126	. . . . . . . 8 |- (A.x x = z -> -. A.z x e. y)
55	54	intnanrd 691	. . . . . . 7 |- (A.x x = z -> -. (A.z x e. y /\ A.yph))
56	52, 55	nexd 1078	. . . . . 6 |- (A.x x = z -> -. E.x(A.z x e. y /\ A.yph))
57	38, 51, 56	sylanc 471	. . . . 5 |- (A.x x = z -> (A.y z e. x <-> E.x(A.z x e. y /\ A.yph)))
58	50, 57	19.21ai 974	. . . 4 |- (A.x x = z