Theorem axrepndlem2 9415

Description: Lemma for the Axiom of Replacement with no distinct variable conditions. (Contributed by NM, 2-Jan-2002.) (Proof shortened by Mario Carneiro, 6-Dec-2016.)

Assertion

Ref	Expression
axrepndlem2	|- ( ( ( -. A. x x = y /\ -. A. x x = z ) /\ -. 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 ) ) ) )

Proof of Theorem axrepndlem2

Dummy variable w is distinct from all other variables.

Step	Hyp	Ref	Expression
1		axrepndlem1 9414	. . 3 |- ( -. A. y y = z -> E. w ( E. y A. z ( [ w / x ] ph -> z = y ) -> A. z ( z e. w <-> E. w ( w e. y /\ A. y [ w / x ] ph ) ) ) )
2		nfnae 2318	. . . . 5 |- F/ x -. A. x x = y
3		nfnae 2318	. . . . 5 |- F/ x -. A. x x = z
4	2, 3	nfan 1828	. . . 4 |- F/ x ( -. A. x x = y /\ -. A. x x = z )
5		nfnae 2318	. . . . . . 7 |- F/ y -. A. x x = y
6		nfnae 2318	. . . . . . 7 |- F/ y -. A. x x = z
7	5, 6	nfan 1828	. . . . . 6 |- F/ y ( -. A. x x = y /\ -. A. x x = z )
8		nfnae 2318	. . . . . . . 8 |- F/ z -. A. x x = y
9		nfnae 2318	. . . . . . . 8 |- F/ z -. A. x x = z
10	8, 9	nfan 1828	. . . . . . 7 |- F/ z ( -. A. x x = y /\ -. A. x x = z )
11		nfs1v 2437	. . . . . . . . 9 |- F/ x [ w / x ] ph
12	11	a1i 11	. . . . . . . 8 |- ( ( -. A. x x = y /\ -. A. x x = z ) -> F/ x [ w / x ] ph )
13		nfcvf 2788	. . . . . . . . . 10 |- ( -. A. x x = z -> F/_ x z )
14	13	adantl 482	. . . . . . . . 9 |- ( ( -. A. x x = y /\ -. A. x x = z ) -> F/_ x z )
15		nfcvf 2788	. . . . . . . . . 10 |- ( -. A. x x = y -> F/_ x y )
16	15	adantr 481	. . . . . . . . 9 |- ( ( -. A. x x = y /\ -. A. x x = z ) -> F/_ x y )
17	14, 16	nfeqd 2772	. . . . . . . 8 |- ( ( -. A. x x = y /\ -. A. x x = z ) -> F/ x z = y )
18	12, 17	nfimd 1823	. . . . . . 7 |- ( ( -. A. x x = y /\ -. A. x x = z ) -> F/ x ( [ w / x ] ph -> z = y ) )
19	10, 18	nfald 2165	. . . . . 6 |- ( ( -. A. x x = y /\ -. A. x x = z ) -> F/ x A. z ( [ w / x ] ph -> z = y ) )
20	7, 19	nfexd 2167	. . . . 5 |- ( ( -. A. x x = y /\ -. A. x x = z ) -> F/ x E. y A. z ( [ w / x ] ph -> z = y ) )
21		nfcvd 2765	. . . . . . . 8 |- ( ( -. A. x x = y /\ -. A. x x = z ) -> F/_ x w )
22	14, 21	nfeld 2773	. . . . . . 7 |- ( ( -. A. x x = y /\ -. A. x x = z ) -> F/ x z e. w )
23		nfv 1843	. . . . . . . 8 |- F/ w ( -. A. x x = y /\ -. A. x x = z )
24	21, 16	nfeld 2773	. . . . . . . . 9 |- ( ( -. A. x x = y /\ -. A. x x = z ) -> F/ x w e. y )
25	7, 12	nfald 2165	. . . . . . . . 9 |- ( ( -. A. x x = y /\ -. A. x x = z ) -> F/ x A. y [ w / x ] ph )
26	24, 25	nfand 1826	. . . . . . . 8 |- ( ( -. A. x x = y /\ -. A. x x = z ) -> F/ x ( w e. y /\ A. y [ w / x ] ph ) )
27	23, 26	nfexd 2167	. . . . . . 7 |- ( ( -. A. x x = y /\ -. A. x x = z ) -> F/ x E. w ( w e. y /\ A. y [ w / x ] ph ) )
28	22, 27	nfbid 1832	. . . . . 6 |- ( ( -. A. x x = y /\ -. A. x x = z ) -> F/ x ( z e. w <-> E. w ( w e. y /\ A. y [ w / x ] ph ) ) )
29	10, 28	nfald 2165	. . . . 5 |- ( ( -. A. x x = y /\ -. A. x x = z ) -> F/ x A. z ( z e. w <-> E. w ( w e. y /\ A. y [ w / x ] ph ) ) )
30	20, 29	nfimd 1823	. . . 4 |- ( ( -. A. x x = y /\ -. A. x x = z ) -> F/ x ( E. y A. z ( [ w / x ] ph -> z = y ) -> A. z ( z e. w <-> E. w ( w e. y /\ A. y [ w / x ] ph ) ) ) )
31		nfcvd 2765	. . . . . . . . 9 |- ( ( -. A. x x = y /\ -. A. x x = z ) -> F/_ y w )
32		nfcvf2 2789	. . . . . . . . . 10 |- ( -. A. x x = y -> F/_ y x )
33	32	adantr 481	. . . . . . . . 9 |- ( ( -. A. x x = y /\ -. A. x x = z ) -> F/_ y x )
34	31, 33	nfeqd 2772	. . . . . . . 8 |- ( ( -. A. x x = y /\ -. A. x x = z ) -> F/ y w = x )
35	7, 34	nfan1 2068	. . . . . . 7 |- F/ y ( ( -. A. x x = y /\ -. A. x x = z ) /\ w = x )
36		nfcvd 2765	. . . . . . . . . 10 |- ( ( -. A. x x = y /\ -. A. x x = z ) -> F/_ z w )
37		nfcvf2 2789	. . . . . . . . . . 11 |- ( -. A. x x = z -> F/_ z x )
38	37	adantl 482	. . . . . . . . . 10 |- ( ( -. A. x x = y /\ -. A. x x = z ) -> F/_ z x )
39	36, 38	nfeqd 2772	. . . . . . . . 9 |- ( ( -. A. x x = y /\ -. A. x x = z ) -> F/ z w = x )
40	10, 39	nfan1 2068	. . . . . . . 8 |- F/ z ( ( -. A. x x = y /\ -. A. x x = z ) /\ w = x )
41		sbequ12r 2112	. . . . . . . . . 10 |- ( w = x -> ( [ w / x ] ph <-> ph ) )
42	41	imbi1d 331	. . . . . . . . 9 |- ( w = x -> ( ( [ w / x ] ph -> z = y ) <-> ( ph -> z = y ) ) )
43	42	adantl 482	. . . . . . . 8 |- ( ( ( -. A. x x = y /\ -. A. x x = z ) /\ w = x ) -> ( ( [ w / x ] ph -> z = y ) <-> ( ph -> z = y ) ) )
44	40, 43	albid 2090	. . . . . . 7 |- ( ( ( -. A. x x = y /\ -. A. x x = z ) /\ w = x ) -> ( A. z ( [ w / x ] ph -> z = y ) <-> A. z ( ph -> z = y ) ) )
45	35, 44	exbid 2091	. . . . . 6 |- ( ( ( -. A. x x = y /\ -. A. x x = z ) /\ w = x ) -> ( E. y A. z ( [ w / x ] ph -> z = y ) <-> E. y A. z ( ph -> z = y ) ) )
46		elequ2 2004	. . . . . . . . 9 |- ( w = x -> ( z e. w <-> z e. x ) )
47	46	adantl 482	. . . . . . . 8 |- ( ( ( -. A. x x = y /\ -. A. x x = z ) /\ w = x ) -> ( z e. w <-> z e. x ) )
48		elequ1 1997	. . . . . . . . . . . . 13 |- ( w = x -> ( w e. y <-> x e. y ) )
49	48	adantl 482	. . . . . . . . . . . 12 |- ( ( ( -. A. x x = y /\ -. A. x x = z ) /\ w = x ) -> ( w e. y <-> x e. y ) )
50	41	adantl 482	. . . . . . . . . . . . 13 |- ( ( ( -. A. x x = y /\ -. A. x x = z ) /\ w = x ) -> ( [ w / x ] ph <-> ph ) )
51	35, 50	albid 2090	. . . . . . . . . . . 12 |- ( ( ( -. A. x x = y /\ -. A. x x = z ) /\ w = x ) -> ( A. y [ w / x ] ph <-> A. y ph ) )
52	49, 51	anbi12d 747	. . . . . . . . . . 11 |- ( ( ( -. A. x x = y /\ -. A. x x = z ) /\ w = x ) -> ( ( w e. y /\ A. y [ w / x ] ph ) <-> ( x e. y /\ A. y ph ) ) )
53	52	ex 450	. . . . . . . . . 10 |- ( ( -. A. x x = y /\ -. A. x x = z ) -> ( w = x -> ( ( w e. y /\ A. y [ w / x ] ph ) <-> ( x e. y /\ A. y ph ) ) ) )
54	4, 26, 53	cbvexd 2278	. . . . . . . . 9 |- ( ( -. A. x x = y /\ -. A. x x = z ) -> ( E. w ( w e. y /\ A. y [ w / x ] ph ) <-> E. x ( x e. y /\ A. y ph ) ) )
55	54	adantr 481	. . . . . . . 8 |- ( ( ( -. A. x x = y /\ -. A. x x = z ) /\ w = x ) -> ( E. w ( w e. y /\ A. y [ w / x ] ph ) <-> E. x ( x e. y /\ A. y ph ) ) )
56	47, 55	bibi12d 335	. . . . . . 7 |- ( ( ( -. A. x x = y /\ -. A. x x = z ) /\ w = x ) -> ( ( z e. w <-> E. w ( w e. y /\ A. y [ w / x ] ph ) ) <-> ( z e. x <-> E. x ( x e. y /\ A. y ph ) ) ) )
57	40, 56	albid 2090	. . . . . 6 |- ( ( ( -. A. x x = y /\ -. A. x x = z ) /\ w = x ) -> ( A. z ( z e. w <-> E. w ( w e. y /\ A. y [ w / x ] ph ) ) <-> A. z ( z e. x <-> E. x ( x e. y /\ A. y ph ) ) ) )
58	45, 57	imbi12d 334	. . . . 5 |- ( ( ( -. A. x x = y /\ -. A. x x = z ) /\ w = x ) -> ( ( E. y A. z ( [ w / x ] ph -> z = y ) -> A. z ( z e. w <-> E. w ( w e. y /\ A. y [ w / x ] ph ) ) ) <-> ( E. y A. z ( ph -> z = y ) -> A. z ( z e. x <-> E. x ( x e. y /\ A. y ph ) ) ) ) )
59	58	ex 450	. . . 4 |- ( ( -. A. x x = y /\ -. A. x x = z ) -> ( w = x -> ( ( E. y A. z ( [ w / x ] ph -> z = y ) -> A. z ( z e. w <-> E. w ( w e. y /\ A. y [ w / x ] ph ) ) ) <-> ( E. y A. z ( ph -> z = y ) -> A. z ( z e. x <-> E. x ( x e. y /\ A. y ph ) ) ) ) ) )
60	4, 30, 59	cbvexd 2278	. . 3 |- ( ( -. A. x x = y /\ -. A. x x = z ) -> ( E. w ( E. y A. z ( [ w / x ] ph -> z = y ) -> A. z ( z e. w <-> E. w ( w e. y /\ A. y [ w / x ] ph ) ) ) <-> E. x ( E. y A. z ( ph -> z = y ) -> A. z ( z e. x <-> E. x ( x e. y /\ A. y ph ) ) ) ) )
61	1, 60	syl5ib 234	. 2 |- ( ( -. A. x x = y /\ -. A. x x = z ) -> ( -. 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 ) ) ) ) )
62	61	imp 445	1 |- ( ( ( -. A. x x = y /\ -. A. x x = z ) /\ -. 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   F/_wnfc 2751

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:  axrepnd  9416