Theorem axrep1 4772

Description: The version of the Axiom of Replacement used in the Metamath Solitaire applet http://us.metamath.org/mmsolitaire/mms.html. Equivalence is shown via the path ax-rep 4771 -> axrep1 4772 -> axrep2 4773 -> axrepnd 9416 -> zfcndrep 9436 = ax-rep 4771. (Contributed by NM, 19-Nov-2005.) (Proof shortened by Mario Carneiro, 17-Nov-2016.)

Assertion

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

Distinct variable groups:   ph, y   x, y, z

Allowed substitution hints:   ph( x, z)

Proof of Theorem axrep1

Dummy variable w is distinct from all other variables.

Step	Hyp	Ref	Expression
1		elequ2 2004	. . . . . . . . 9 |- ( w = y -> ( x e. w <-> x e. y ) )
2	1	anbi1d 741	. . . . . . . 8 |- ( w = y -> ( ( x e. w /\ ph ) <-> ( x e. y /\ ph ) ) )
3	2	exbidv 1850	. . . . . . 7 |- ( w = y -> ( E. x ( x e. w /\ ph ) <-> E. x ( x e. y /\ ph ) ) )
4	3	bibi2d 332	. . . . . 6 |- ( w = y -> ( ( z e. x <-> E. x ( x e. w /\ ph ) ) <-> ( z e. x <-> E. x ( x e. y /\ ph ) ) ) )
5	4	albidv 1849	. . . . 5 |- ( w = y -> ( A. z ( z e. x <-> E. x ( x e. w /\ ph ) ) <-> A. z ( z e. x <-> E. x ( x e. y /\ ph ) ) ) )
6	5	exbidv 1850	. . . 4 |- ( w = y -> ( E. x A. z ( z e. x <-> E. x ( x e. w /\ ph ) ) <-> E. x A. z ( z e. x <-> E. x ( x e. y /\ ph ) ) ) )
7	6	imbi2d 330	. . 3 |- ( w = y -> ( ( A. x E. y A. z ( ph -> z = y ) -> E. x A. z ( z e. x <-> E. x ( x e. w /\ ph ) ) ) <-> ( A. x E. y A. z ( ph -> z = y ) -> E. x A. z ( z e. x <-> E. x ( x e. y /\ ph ) ) ) ) )
8		ax-rep 4771	. . . 4 |- ( A. x E. y A. z ( A. y ph -> z = y ) -> E. y A. z ( z e. y <-> E. x ( x e. w /\ A. y ph ) ) )
9		19.3v 1897	. . . . . . . 8 |- ( A. y ph <-> ph )
10	9	imbi1i 339	. . . . . . 7 |- ( ( A. y ph -> z = y ) <-> ( ph -> z = y ) )
11	10	albii 1747	. . . . . 6 |- ( A. z ( A. y ph -> z = y ) <-> A. z ( ph -> z = y ) )
12	11	exbii 1774	. . . . 5 |- ( E. y A. z ( A. y ph -> z = y ) <-> E. y A. z ( ph -> z = y ) )
13	12	albii 1747	. . . 4 |- ( A. x E. y A. z ( A. y ph -> z = y ) <-> A. x E. y A. z ( ph -> z = y ) )
14		nfv 1843	. . . . . . 7 |- F/ x z e. y
15		nfe1 2027	. . . . . . 7 |- F/ x E. x ( x e. w /\ A. y ph )
16	14, 15	nfbi 1833	. . . . . 6 |- F/ x ( z e. y <-> E. x ( x e. w /\ A. y ph ) )
17	16	nfal 2153	. . . . 5 |- F/ x A. z ( z e. y <-> E. x ( x e. w /\ A. y ph ) )
18		nfv 1843	. . . . 5 |- F/ y A. z ( z e. x <-> E. x ( x e. w /\ ph ) )
19		elequ2 2004	. . . . . . 7 |- ( y = x -> ( z e. y <-> z e. x ) )
20	9	anbi2i 730	. . . . . . . . 9 |- ( ( x e. w /\ A. y ph ) <-> ( x e. w /\ ph ) )
21	20	exbii 1774	. . . . . . . 8 |- ( E. x ( x e. w /\ A. y ph ) <-> E. x ( x e. w /\ ph ) )
22	21	a1i 11	. . . . . . 7 |- ( y = x -> ( E. x ( x e. w /\ A. y ph ) <-> E. x ( x e. w /\ ph ) ) )
23	19, 22	bibi12d 335	. . . . . 6 |- ( y = x -> ( ( z e. y <-> E. x ( x e. w /\ A. y ph ) ) <-> ( z e. x <-> E. x ( x e. w /\ ph ) ) ) )
24	23	albidv 1849	. . . . 5 |- ( y = x -> ( A. z ( z e. y <-> E. x ( x e. w /\ A. y ph ) ) <-> A. z ( z e. x <-> E. x ( x e. w /\ ph ) ) ) )
25	17, 18, 24	cbvex 2272	. . . 4 |- ( E. y A. z ( z e. y <-> E. x ( x e. w /\ A. y ph ) ) <-> E. x A. z ( z e. x <-> E. x ( x e. w /\ ph ) ) )
26	8, 13, 25	3imtr3i 280	. . 3 |- ( A. x E. y A. z ( ph -> z = y ) -> E. x A. z ( z e. x <-> E. x ( x e. w /\ ph ) ) )
27	7, 26	chvarv 2263	. 2 |- ( A. x E. y A. z ( ph -> z = y ) -> E. x A. z ( z e. x <-> E. x ( x e. y /\ ph ) ) )
28	27	19.35ri 1807	1 |- E. x ( E. y A. z ( ph -> z = y ) -> A. z ( z e. x <-> E. x ( x e. 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:  axrep2  4773