Theorem axrep4 2702

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 2701	. . 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 1078	. 2 |- (A.xE.zA.y(ph -> y = z) -> E.xA.y(y e. x <-> E.x(x e. w /\ A.zph)))
3		ax-17 973	. . . . 5 |- (y e. x -> A.z y e. x)
4		ax-17 973	. . . . . . 7 |- (x e. w -> A.z x e. w)
5		hba1 1005	. . . . . . 7 |- (A.zph -> A.zA.zph)
6	4, 5	hban 1011	. . . . . 6 |- ((x e. w /\ A.zph) -> A.z(x e. w /\ A.zph))
7	6	hbex 1008	. . . . 5 |- (E.x(x e. w /\ A.zph) -> A.zE.x(x e. w /\ A.zph))
8	3, 7	hbbi 1012	. . . 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 1007	. . 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 973	. . . . 5 |- (y e. z -> A.x y e. z)
11		hbe1 1018	. . . . 5 |- (E.x(x e. w /\ ph) -> A.xE.x(x e. w /\ ph))
12	10, 11	hbbi 1012	. . . 4 |- ((y e. z <-> E.x(x e. w /\ ph)) -> A.x(y e. z <-> E.x(x e. w /\ ph)))
13	12	hbal 1007	. . 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 973	. . . 4 |- (x = z -> A.y x = z)
15		elequ2 1139	. . . . 5 |- (x = z -> (y e. x <-> y e. z))
16		axrep4.1	. . . . . . . . 9 |- (ph -> A.zph)
17	16	19.3 1033	. . . . . . . 8 |- (A.zph <-> ph)
18	17	anbi2i 482	. . . . . . 7 |- ((x e. w /\ A.zph) <-> (x e. w /\ ph))
19	18	exbii 1053	. . . . . 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 631	. . . 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 1106	. . 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 1168	. 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 956   = wceq 958   e. wcel 960  E.wex 982

This theorem is referenced by:  axrep5 2703  funimaexg 3581

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 964  ax-gen 965  ax-8 966  ax-12 970  ax-14 972  ax-17 973  ax-4 975  ax-5o 977  ax-6o 980  ax-9o 1125  ax-rep 2698

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

Copyright terms: Public domain