Theorem axrepnd 3740

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 3739	. . . 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		eq6 826	. . . . . . 7 |- (-. A.x x = y -> A.x -. A.x x = y)
3		eq6 826	. . . . . . 7 |- (-. A.x x = z -> A.x -. A.x x = z)
4	2, 3	hban 704	. . . . . 6 |- ((-. A.x x = y /\ -. A.x x = z) -> A.x(-. A.x x = y /\ -. A.x x = z))
5		eq6 826	. . . . . 6 |- (-. A.y y = z -> A.x -. A.y y = z)
6	4, 5	hban 704	. . . . 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		eq6 826	. . . . . . . . 9 |- (-. A.x x = y -> A.z -. A.x x = y)
8		eq6 826	. . . . . . . . 9 |- (-. A.x x = z -> A.z -. A.x x = z)
9	7, 8	hban 704	. . . . . . . 8 |- ((-. A.x x = y /\ -. A.x x = z) -> A.z(-. A.x x = y /\ -. A.x x = z))
10		eq6 826	. . . . . . . 8 |- (-. A.y y = z -> A.z -. A.y y = z)
11	9, 10	hban 704	. . . . . . 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 1006	. . . . . . . . . . . . 13 |- (-. A.y y = z -> (-. A.y y = x -> (z e. x -> A.y z e. x)))
13	12	com12 13	. . . . . . . . . . . 12 |- (-. A.y y = x -> (-. A.y y = z -> (z e. x -> A.y z e. x)))
14	13	eq4ds 823	. . . . . . . . . . 11 |- (-. A.x x = y -> (-. A.y y = z -> (z e. x -> A.y z e. x)))
15	14	imp 277	. . . . . . . . . 10 |- ((-. A.x x = y /\ -. A.y y = z) -> (z e. x -> A.y z e. x))
16	15	adantlr 310	. . . . . . . . 9 |- (((-. A.x x = y /\ -. A.x x = z) /\ -. A.y y = z) -> (z e. x -> A.y z e. x))
17		ax-4 673	. . . . . . . . . 10 |- (A.y z e. x -> z e. x)
18	17	a1i 7	. . . . . . . . 9 |- (((-. A.x x = y /\ -. A.x x = z) /\ -. A.y y = z) -> (A.y z e. x -> z e. x))
19	16, 18	impbid 397	. . . . . . . 8 |- (((-. A.x x = y /\ -. A.x x = z) /\ -. A.y y = z) -> (z e. x <-> A.y z e. x))
20		ax15 1006	. . . . . . . . . . . . . 14 |- (-. A.z z = x -> (-. A.z z = y -> (x e. y -> A.z x e. y)))
21	20	imp 277	. . . . . . . . . . . . 13 |- ((-. A.z z = x /\ -. A.z z = y) -> (x e. y -> A.z x e. y))
22		eq4 821	. . . . . . . . . . . . . 14 |- (A.z z = x -> A.x x = z)
23	22	con3i 90	. . . . . . . . . . . . 13 |- (-. A.x x = z -> -. A.z z = x)
24		eq4 821	. . . . . . . . . . . . . 14 |- (A.z z = y -> A.y y = z)
25	24	con3i 90	. . . . . . . . . . . . 13 |- (-. A.y y = z -> -. A.z z = y)
26	21, 23, 25	syl2an 349	. . . . . . . . . . . 12 |- ((-. A.x x = z /\ -. A.y y = z) -> (x e. y -> A.z x e. y))
27	26	adantll 309	. . . . . . . . . . 11 |- (((-. A.x x = y /\ -. A.x x = z) /\ -. A.y y = z) -> (x e. y -> A.z x e. y))
28		ax-4 673	. . . . . . . . . . . 12 |- (A.z x e. y -> x e. y)
29	28	a1i 7	. . . . . . . . . . 11 |- (((-. A.x x = y /\ -. A.x x = z) /\ -. A.y y = z) -> (A.z x e. y -> x e. y))
30	27, 29	impbid 397	. . . . . . . . . 10 |- (((-. A.x x = y /\ -. A.x x = z) /\ -. A.y y = z) -> (x e. y <-> A.z x e. y))
31	30	anbi1d 469	. . . . . . . . 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)))
32	6, 31	biexd 783	. . . . . . . 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)))
33	19, 32	bibi12d 477	. . . . . . 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))))
34	11, 33	biald 782	. . . . . 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))))
35	34	imbi2d 464	. . . . 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)))))
36	6, 35	biexd 783	. . . 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)))))
37	1, 36	mpbid 170	. . 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))))
38	37	exp31 293	. 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))))))
39		eq5 824	. . . . 5 |- (A.x x = y -> A.zA.x x = y)
40		pm5.21 502	. . . . . 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)))
41		nd2 3733	. . . . . . 7 |- (A.y y = x -> -. A.y z e. x)
42	41	eq4s 822	. . . . . 6 |- (A.x x = y -> -. A.y z e. x)
43		eq5 824	. . . . . . 7 |- (A.x x = y -> A.xA.x x = y)
44		nd3 3734	. . . . . . . 8 |- (A.x x = y -> -. A.z x e. y)
45		pm3.26 256	. . . . . . . 8 |- ((A.z x e. y /\ A.yph) -> A.z x e. y)
46	44, 45	nsyl 102	. . . . . . 7 |- (A.x x = y -> -. (A.z x e. y /\ A.yph))
47	43, 46	nexd 780	. . . . . 6 |- (A.x x = y -> -. E.x(A.z x e. y /\ A.yph))
48	40, 42, 47	sylanc 361	. . . . 5 |- (A.x x = y -> (A.y z e. x <-> E.x(A.z x e. y /\ A.yph)))
49	39, 48	19.21ai 740	. . . 4 |- (A.x x = y -> A.z(A.y z e. x <-> E.x(A.z x e. y /\ A.yph)))
50	49	a1d 14	. . 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))))
51		19.8a 712	. . 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))))
52	50, 51	syl 12	. 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))))
53		eq5 824	. . . . 5 |- (A.x x = z -> A.zA.x x = z)
54		nd4 3735	. . . . . 6 |- (A.x x = z -> -. A.y z e. x)
55		eq5 824	. . . . . . 7 |- (A.x x = z -> A.xA.x x = z)
56		nd1 3732	. . . . . . . . 9 |- (A.z z = x -> -. A.z x e. y)
57	56	eq4s 822	. . . . . . . 8 |- (A.x x = z -> -. A.z x e. y)
58	57, 45	nsyl 102	. . . . . . 7 |- (A.x x = z -> -. (A.z x e. y /\ A.yph))
59	55, 58	nexd 780	. . . . . 6 |- (A.x x = z -> -. E.x(A.z x e. y /\ A.yph))
60	40, 54, 59	sylanc 361	. . . . 5 |- (A.x x = z -> (A.y z e. x <->