Theorem axrepndlem1 9414

Description: Lemma for the Axiom of Replacement with no distinct variable conditions. (Contributed by NM, 2-Jan-2002.)

Assertion

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

Distinct variable groups:   x, z   x, y

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

Proof of Theorem axrepndlem1

Dummy variable w is distinct from all other variables.

Step	Hyp	Ref	Expression
1		axrep2 4773	. 2 |- E. x ( E. y A. w ( [ w / z ] ph -> w = y ) -> A. w ( w e. x <-> E. x ( x e. y /\ A. y [ w / z ] ph ) ) )
2		nfnae 2318	. . 3 |- F/ x -. A. y y = z
3		nfnae 2318	. . . . 5 |- F/ y -. A. y y = z
4		nfnae 2318	. . . . . 6 |- F/ z -. A. y y = z
5		nfs1v 2437	. . . . . . . 8 |- F/ z [ w / z ] ph
6	5	a1i 11	. . . . . . 7 |- ( -. A. y y = z -> F/ z [ w / z ] ph )
7		nfcvd 2765	. . . . . . . 8 |- ( -. A. y y = z -> F/_ z w )
8		nfcvf2 2789	. . . . . . . 8 |- ( -. A. y y = z -> F/_ z y )
9	7, 8	nfeqd 2772	. . . . . . 7 |- ( -. A. y y = z -> F/ z w = y )
10	6, 9	nfimd 1823	. . . . . 6 |- ( -. A. y y = z -> F/ z ( [ w / z ] ph -> w = y ) )
11		sbequ12r 2112	. . . . . . . 8 |- ( w = z -> ( [ w / z ] ph <-> ph ) )
12		equequ1 1952	. . . . . . . 8 |- ( w = z -> ( w = y <-> z = y ) )
13	11, 12	imbi12d 334	. . . . . . 7 |- ( w = z -> ( ( [ w / z ] ph -> w = y ) <-> ( ph -> z = y ) ) )
14	13	a1i 11	. . . . . 6 |- ( -. A. y y = z -> ( w = z -> ( ( [ w / z ] ph -> w = y ) <-> ( ph -> z = y ) ) ) )
15	4, 10, 14	cbvald 2277	. . . . 5 |- ( -. A. y y = z -> ( A. w ( [ w / z ] ph -> w = y ) <-> A. z ( ph -> z = y ) ) )
16	3, 15	exbid 2091	. . . 4 |- ( -. A. y y = z -> ( E. y A. w ( [ w / z ] ph -> w = y ) <-> E. y A. z ( ph -> z = y ) ) )
17		nfvd 1844	. . . . . 6 |- ( -. A. y y = z -> F/ z w e. x )
18	8	nfcrd 2771	. . . . . . . 8 |- ( -. A. y y = z -> F/ z x e. y )
19	3, 6	nfald 2165	. . . . . . . 8 |- ( -. A. y y = z -> F/ z A. y [ w / z ] ph )
20	18, 19	nfand 1826	. . . . . . 7 |- ( -. A. y y = z -> F/ z ( x e. y /\ A. y [ w / z ] ph ) )
21	2, 20	nfexd 2167	. . . . . 6 |- ( -. A. y y = z -> F/ z E. x ( x e. y /\ A. y [ w / z ] ph ) )
22	17, 21	nfbid 1832	. . . . 5 |- ( -. A. y y = z -> F/ z ( w e. x <-> E. x ( x e. y /\ A. y [ w / z ] ph ) ) )
23		elequ1 1997	. . . . . . . 8 |- ( w = z -> ( w e. x <-> z e. x ) )
24	23	adantl 482	. . . . . . 7 |- ( ( -. A. y y = z /\ w = z ) -> ( w e. x <-> z e. x ) )
25		nfeqf2 2297	. . . . . . . . . . 11 |- ( -. A. y y = z -> F/ y w = z )
26	3, 25	nfan1 2068	. . . . . . . . . 10 |- F/ y ( -. A. y y = z /\ w = z )
27	11	adantl 482	. . . . . . . . . 10 |- ( ( -. A. y y = z /\ w = z ) -> ( [ w / z ] ph <-> ph ) )
28	26, 27	albid 2090	. . . . . . . . 9 |- ( ( -. A. y y = z /\ w = z ) -> ( A. y [ w / z ] ph <-> A. y ph ) )
29	28	anbi2d 740	. . . . . . . 8 |- ( ( -. A. y y = z /\ w = z ) -> ( ( x e. y /\ A. y [ w / z ] ph ) <-> ( x e. y /\ A. y ph ) ) )
30	29	exbidv 1850	. . . . . . 7 |- ( ( -. A. y y = z /\ w = z ) -> ( E. x ( x e. y /\ A. y [ w / z ] ph ) <-> E. x ( x e. y /\ A. y ph ) ) )
31	24, 30	bibi12d 335	. . . . . 6 |- ( ( -. A. y y = z /\ w = z ) -> ( ( w e. x <-> E. x ( x e. y /\ A. y [ w / z ] ph ) ) <-> ( z e. x <-> E. x ( x e. y /\ A. y ph ) ) ) )
32	31	ex 450	. . . . 5 |- ( -. A. y y = z -> ( w = z -> ( ( w e. x <-> E. x ( x e. y /\ A. y [ w / z ] ph ) ) <-> ( z e. x <-> E. x ( x e. y /\ A. y ph ) ) ) ) )
33	4, 22, 32	cbvald 2277	. . . 4 |- ( -. A. y y = z -> ( A. w ( w e. x <-> E. x ( x e. y /\ A. y [ w / z ] ph ) ) <-> A. z ( z e. x <-> E. x ( x e. y /\ A. y ph ) ) ) )
34	16, 33	imbi12d 334	. . 3 |- ( -. A. y y = z -> ( ( E. y A. w ( [ w / z ] ph -> w = y ) -> A. w ( w e. x <-> E. x ( x e. y /\ A. y [ w / z ] ph ) ) ) <-> ( E. y A. z ( ph -> z = y ) -> A. z ( z e. x <-> E. x ( x e. y /\ A. y ph ) ) ) ) )
35	2, 34	exbid 2091	. 2 |- ( -. A. y y = z -> ( E. x ( E. y A. w ( [ w / z ] ph -> w = y ) -> A. w ( w e. x <-> E. x ( x e. y /\ A. y [ w / z ] ph ) ) ) <-> E. x ( E. y A. z ( ph -> z = y ) -> A. z ( z e. x <-> E. x ( x e. y /\ A. y ph ) ) ) ) )
36	1, 35	mpbii 223	1 |- ( -. A. y y = z -> E. x ( E. y A. z ( ph -> z = y ) -> A. z ( z e. x <-> E. x ( x e. y /\ A. y ph ) ) ) )

Syntax hints:   -. wn 3   -> wi 4   <-> wb 196   /\ wa 384   A.wal 1481   E.wex 1704   F/wnf 1708   [wsb 1880

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-8 1992  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602  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  df-sb 1881  df-cleq 2615  df-clel 2618  df-nfc 2753

This theorem is referenced by:  axrepndlem2  9415