Theorem axrep2 4773

Description: Axiom of Replacement expressed with the fewest number of different variables and without any restrictions on ph. (Contributed by NM, 15-Aug-2003.)

Assertion

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

Distinct variable group:   x, y, z

Allowed substitution hints:   ph( x, y, z)

Proof of Theorem axrep2

Dummy variable w is distinct from all other variables.

Step	Hyp	Ref	Expression
1		nfe1 2027	. . . . 5 |- F/ w E. w A. z ( A. y ph -> z = w )
2		nfv 1843	. . . . 5 |- F/ w A. z ( z e. x <-> E. x ( x e. y /\ A. y ph ) )
3	1, 2	nfim 1825	. . . 4 |- F/ w ( E. w A. z ( A. y ph -> z = w ) -> A. z ( z e. x <-> E. x ( x e. y /\ A. y ph ) ) )
4	3	nfex 2154	. . 3 |- F/ w E. x ( E. w A. z ( A. y ph -> z = w ) -> A. z ( z e. x <-> E. x ( x e. y /\ A. y ph ) ) )
5		elequ2 2004	. . . . . . . . 9 |- ( w = y -> ( x e. w <-> x e. y ) )
6	5	anbi1d 741	. . . . . . . 8 |- ( w = y -> ( ( x e. w /\ A. y ph ) <-> ( x e. y /\ A. y ph ) ) )
7	6	exbidv 1850	. . . . . . 7 |- ( w = y -> ( E. x ( x e. w /\ A. y ph ) <-> E. x ( x e. y /\ A. y ph ) ) )
8	7	bibi2d 332	. . . . . 6 |- ( w = y -> ( ( z e. x <-> E. x ( x e. w /\ A. y ph ) ) <-> ( z e. x <-> E. x ( x e. y /\ A. y ph ) ) ) )
9	8	albidv 1849	. . . . 5 |- ( w = y -> ( A. z ( z e. x <-> E. x ( x e. w /\ A. y ph ) ) <-> A. z ( z e. x <-> E. x ( x e. y /\ A. y ph ) ) ) )
10	9	imbi2d 330	. . . 4 |- ( w = y -> ( ( E. w A. z ( A. y ph -> z = w ) -> A. z ( z e. x <-> E. x ( x e. w /\ A. y ph ) ) ) <-> ( E. w A. z ( A. y ph -> z = w ) -> A. z ( z e. x <-> E. x ( x e. y /\ A. y ph ) ) ) ) )
11	10	exbidv 1850	. . 3 |- ( w = y -> ( E. x ( E. w A. z ( A. y ph -> z = w ) -> A. z ( z e. x <-> E. x ( x e. w /\ A. y ph ) ) ) <-> E. x ( E. w A. z ( A. y ph -> z = w ) -> A. z ( z e. x <-> E. x ( x e. y /\ A. y ph ) ) ) ) )
12		axrep1 4772	. . 3 |- E. x ( E. w A. z ( A. y ph -> z = w ) -> A. z ( z e. x <-> E. x ( x e. w /\ A. y ph ) ) )
13	4, 11, 12	chvar 2262	. 2 |- E. x ( E. w A. z ( A. y ph -> z = w ) -> A. z ( z e. x <-> E. x ( x e. y /\ A. y ph ) ) )
14		sp 2053	. . . . . . 7 |- ( A. y ph -> ph )
15	14	imim1i 63	. . . . . 6 |- ( ( ph -> z = y ) -> ( A. y ph -> z = y ) )
16	15	alimi 1739	. . . . 5 |- ( A. z ( ph -> z = y ) -> A. z ( A. y ph -> z = y ) )
17	16	eximi 1762	. . . 4 |- ( E. y A. z ( ph -> z = y ) -> E. y A. z ( A. y ph -> z = y ) )
18		nfv 1843	. . . . 5 |- F/ w A. z ( A. y ph -> z = y )
19		nfa1 2028	. . . . . . 7 |- F/ y A. y ph
20		nfv 1843	. . . . . . 7 |- F/ y z = w
21	19, 20	nfim 1825	. . . . . 6 |- F/ y ( A. y ph -> z = w )
22	21	nfal 2153	. . . . 5 |- F/ y A. z ( A. y ph -> z = w )
23		equequ2 1953	. . . . . . 7 |- ( y = w -> ( z = y <-> z = w ) )
24	23	imbi2d 330	. . . . . 6 |- ( y = w -> ( ( A. y ph -> z = y ) <-> ( A. y ph -> z = w ) ) )
25	24	albidv 1849	. . . . 5 |- ( y = w -> ( A. z ( A. y ph -> z = y ) <-> A. z ( A. y ph -> z = w ) ) )
26	18, 22, 25	cbvex 2272	. . . 4 |- ( E. y A. z ( A. y ph -> z = y ) <-> E. w A. z ( A. y ph -> z = w ) )
27	17, 26	sylib 208	. . 3 |- ( E. y A. z ( ph -> z = y ) -> E. w A. z ( A. y ph -> z = w ) )
28	27	imim1i 63	. 2 |- ( ( E. w A. z ( A. y ph -> z = w ) -> A. z ( z e. x <-> E. x ( x e. y /\ A. y ph ) ) ) -> ( E. y A. z ( ph -> z = y ) -> A. z ( z e. x <-> E. x ( x e. y /\ A. y ph ) ) ) )
29	13, 28	eximii 1764	1 |- E. x ( E. y A. z ( ph -> z = y ) -> A. z ( z e. x <-> E. x ( x e. y /\ A. y ph ) ) )

Syntax hints:   -> wi 4   <-> wb 196   /\ wa 384   A.wal 1481   E.wex 1704

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-rep 4771

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1486  df-ex 1705  df-nf 1710

This theorem is referenced by:  axrep3  4774  axrepndlem1  9414