Theorem axrep4 2692

Description: A more traditional version of the Axiom of Replacement.

Hypothesis

Ref	Expression
axrep4.1	|- (ph -> A.zph)

Assertion

Ref	Expression
axrep4	|- (A.xE.zA.y(ph -> y = z) -> E.zA.y(y e. z <-> E.x(x e. w /\ ph)))

Distinct variable group:   x,y,z,w

Proof of Theorem axrep4

Step	Hyp	Ref	Expression
1		axrep3 2691	. . 3 |- E.x(E.zA.y(ph -> y = z) -> A.y(y e. x <-> E.x(x e. w /\ A.zph)))
2	1	19.35i 1074	. 2 |- (A.xE.zA.y(ph -> y = z) -> E.xA.y(y e. x <-> E.x(x e. w /\ A.zph)))
3		ax-17 969	. . . . 5 |- (y e. x -> A.z y e. x)
4		ax-17 969	. . . . . . 7 |- (x e. w -> A.z x e. w)
5		hba1 1001	. . . . . . 7 |- (A.zph -> A.zA.zph)
6	4, 5	hban 1007	. . . . . 6 |- ((x e. w /\ A.zph) -> A.z(x e. w /\ A.zph))
7	6	hbex 1004	. . . . 5 |- (E.x(x e. w /\ A.zph) -> A.zE.x(x e. w /\ A.zph))
8	3, 7	hbbi 1008	. . . 4 |- ((y e. x <-> E.x(x e. w /\ A.zph)) -> A.z(y e. x <-> E.x(x e. w /\ A.zph)))
9	8	hbal 1003	. . 3 |- (A.y(y e. x <-> E.x(x e. w /\ A.zph)) -> A.zA.y(y e. x <-> E.x(x e. w /\ A.zph)))
10		ax-17 969	. . . . 5 |- (y e. z -> A.x y e. z)
11		hbe1 1014	. . . . 5 |- (E.x(x e. w /\ ph) -> A.xE.x(x e. w /\ ph))
12	10, 11	hbbi 1008	. . . 4 |- ((y e. z <-> E.x(x e. w /\ ph)) -> A.x(y e. z <-> E.x(x e. w /\ ph)))
13	12	hbal 1003	. . 3 |- (A.y(y e. z <-> E.x(x e. w /\ ph)) -> A.xA.y(y e. z <-> E.x(x e. w /\ ph)))
14		ax-17 969	. . . 4 |- (x = z -> A.y x = z)
15		elequ2 1135	. . . . 5 |- (x = z -> (y e. x <-> y e. z))
16		axrep4.1	. . . . . . . . 9 |- (ph -> A.zph)
17	16	19.3 1029	. . . . . . . 8 |- (A.zph <-> ph)
18	17	anbi2i 480	. . . . . . 7 |- ((x e. w /\ A.zph) <-> (x e. w /\ ph))
19	18	exbii 1049	. . . . . 6 |- (E.x(x e. w /\ A.zph) <-> E.x(x e. w /\ ph))
20	19	a1i 8	. . . . 5 |- (x = z -> (E.x(x e. w /\ A.zph) <-> E.x(x e. w /\ ph)))
21	15, 20	bibi12d 628	. . . 4 |- (x = z -> ((y e. x <-> E.x(x e. w /\ A.zph)) <-> (y e. z <-> E.x(x e. w /\ ph))))
22	14, 21	albid 1102	. . 3 |- (x = z -> (A.y(y e. x <-> E.x(x e. w /\ A.zph)) <-> A.y(y e. z <-> E.x(x e. w /\ ph))))
23	9, 13, 22	cbvex 1164	. 2 |- (E.xA.y(y e. x <-> E.x(x e. w /\ A.zph)) <-> E.zA.y(y e. z <-> E.x(x e. w /\ ph)))
24	2, 23	sylib 198	1 |- (A.xE.zA.y(ph -> y = z) -> E.zA.y(y e. z <-> E.x(x e. w /\ ph)))

Syntax hints:   -> wi 3   <-> wb 146   /\ wa 223  A.wal 952   = wceq 954   e. wcel 956  E.wex 978

This theorem is referenced by:  axrep5 2693  funimaexg 3567

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 960  ax-gen 961  ax-8 962  ax-12 966  ax-14 968  ax-17 969  ax-4 971  ax-5o 973  ax-6o 976  ax-9o 1121  ax-rep 2688

This theorem depends on definitions:  df-bi 147  df-an 225  df-ex 979

Copyright terms: Public domain