Theorem axpowndlem2 8781

Description: Lemma for the Axiom of Power Sets with no distinct variable conditions. Revised to remove a redundant antecedent from the consequence. (Contributed by NM, 4-Jan-2002.) (Proof shortened by Mario Carneiro, 6-Dec-2016.) (Revised and shortened by Wolf Lammen, 9-Jun-2019.)

Assertion

Ref	Expression
axpowndlem2	|- ( -. A. x x = y -> ( -. A. x x = z -> E. x A. y ( A. x ( E. z x e. y -> A. y x e. z ) -> y e. x ) ) )

Distinct variable group:   y, z

Proof of Theorem axpowndlem2

Dummy variable w is distinct from all other variables.

Step	Hyp	Ref	Expression
1		zfpow 4490	. . . 4 |- E. w A. y ( A. w ( w e. y -> w e. z ) -> y e. w )
2		19.8a 1793	. . . . . . . . 9 |- ( w e. y -> E. z w e. y )
3		sp 1794	. . . . . . . . 9 |- ( A. y w e. z -> w e. z )
4	2, 3	imim12i 57	. . . . . . . 8 |- ( ( E. z w e. y -> A. y w e. z ) -> ( w e. y -> w e. z ) )
5	4	alimi 1604	. . . . . . 7 |- ( A. w ( E. z w e. y -> A. y w e. z ) -> A. w ( w e. y -> w e. z ) )
6	5	imim1i 58	. . . . . 6 |- ( ( A. w ( w e. y -> w e. z ) -> y e. w ) -> ( A. w ( E. z w e. y -> A. y w e. z ) -> y e. w ) )
7	6	alimi 1604	. . . . 5 |- ( A. y ( A. w ( w e. y -> w e. z ) -> y e. w ) -> A. y ( A. w ( E. z w e. y -> A. y w e. z ) -> y e. w ) )
8	7	eximi 1625	. . . 4 |- ( E. w A. y ( A. w ( w e. y -> w e. z ) -> y e. w ) -> E. w A. y ( A. w ( E. z w e. y -> A. y w e. z ) -> y e. w ) )
9	1, 8	ax-mp 5	. . 3 |- E. w A. y ( A. w ( E. z w e. y -> A. y w e. z ) -> y e. w )
10		nfna1 1837	. . . . 5 |- F/ x -. A. x x = y
11		nfna1 1837	. . . . 5 |- F/ x -. A. x x = z
12	10, 11	nfan 1861	. . . 4 |- F/ x ( -. A. x x = y /\ -. A. x x = z )
13		nfnae 2005	. . . . . 6 |- F/ y -. A. x x = y
14		nfnae 2005	. . . . . 6 |- F/ y -. A. x x = z
15	13, 14	nfan 1861	. . . . 5 |- F/ y ( -. A. x x = y /\ -. A. x x = z )
16		nfv 1673	. . . . . . 7 |- F/ w ( -. A. x x = y /\ -. A. x x = z )
17		nfnae 2005	. . . . . . . . . 10 |- F/ z -. A. x x = y
18		nfcvd 2590	. . . . . . . . . . 11 |- ( -. A. x x = y -> F/_ x w )
19		nfcvf 2613	. . . . . . . . . . 11 |- ( -. A. x x = y -> F/_ x y )
20	18, 19	nfeld 2597	. . . . . . . . . 10 |- ( -. A. x x = y -> F/ x w e. y )
21	17, 20	nfexd 1878	. . . . . . . . 9 |- ( -. A. x x = y -> F/ x E. z w e. y )
22	21	adantr 465	. . . . . . . 8 |- ( ( -. A. x x = y /\ -. A. x x = z ) -> F/ x E. z w e. y )
23		nfcvd 2590	. . . . . . . . . . 11 |- ( -. A. x x = z -> F/_ x w )
24		nfcvf 2613	. . . . . . . . . . 11 |- ( -. A. x x = z -> F/_ x z )
25	23, 24	nfeld 2597	. . . . . . . . . 10 |- ( -. A. x x = z -> F/ x w e. z )
26	14, 25	nfald 1877	. . . . . . . . 9 |- ( -. A. x x = z -> F/ x A. y w e. z )
27	26	adantl 466	. . . . . . . 8 |- ( ( -. A. x x = y /\ -. A. x x = z ) -> F/ x A. y w e. z )
28	22, 27	nfimd 1850	. . . . . . 7 |- ( ( -. A. x x = y /\ -. A. x x = z ) -> F/ x ( E. z w e. y -> A. y w e. z ) )
29	16, 28	nfald 1877	. . . . . 6 |- ( ( -. A. x x = y /\ -. A. x x = z ) -> F/ x A. w ( E. z w e. y -> A. y w e. z ) )
30	19, 18	nfeld 2597	. . . . . . 7 |- ( -. A. x x = y -> F/ x y e. w )
31	30	adantr 465	. . . . . 6 |- ( ( -. A. x x = y /\ -. A. x x = z ) -> F/ x y e. w )
32	29, 31	nfimd 1850	. . . . 5 |- ( ( -. A. x x = y /\ -. A. x x = z ) -> F/ x ( A. w ( E. z w e. y -> A. y w e. z ) -> y e. w ) )
33	15, 32	nfald 1877	. . . 4 |- ( ( -. A. x x = y /\ -. A. x x = z ) -> F/ x A. y ( A. w ( E. z w e. y -> A. y w e. z ) -> y e. w ) )
34		nfeqf2 1989	. . . . . . . . 9 |- ( -. A. y y = x -> F/ y w = x )
35	34	naecoms 2000	. . . . . . . 8 |- ( -. A. x x = y -> F/ y w = x )
36	35	adantr 465	. . . . . . 7 |- ( ( -. A. x x = y /\ -. A. x x = z ) -> F/ y w = x )
37	15, 36	nfan1 1860	. . . . . 6 |- F/ y ( ( -. A. x x = y /\ -. A. x x = z ) /\ w = x )
38		nfnae 2005	. . . . . . . . . . . . . 14 |- F/ z -. A. x x = z
39		nfeqf2 1989	. . . . . . . . . . . . . . 15 |- ( -. A. z z = x -> F/ z w = x )
40	39	naecoms 2000	. . . . . . . . . . . . . 14 |- ( -. A. x x = z -> F/ z w = x )
41	38, 40	nfan1 1860	. . . . . . . . . . . . 13 |- F/ z ( -. A. x x = z /\ w = x )
42		elequ1 1759	. . . . . . . . . . . . . 14 |- ( w = x -> ( w e. y <-> x e. y ) )
43	42	adantl 466	. . . . . . . . . . . . 13 |- ( ( -. A. x x = z /\ w = x ) -> ( w e. y <-> x e. y ) )
44	41, 43	exbid 1820	. . . . . . . . . . . 12 |- ( ( -. A. x x = z /\ w = x ) -> ( E. z w e. y <-> E. z x e. y ) )
45	44	adantll 713	. . . . . . . . . . 11 |- ( ( ( -. A. x x = y /\ -. A. x x = z ) /\ w = x ) -> ( E. z w e. y <-> E. z x e. y ) )
46	13, 35	nfan1 1860	. . . . . . . . . . . . 13 |- F/ y ( -. A. x x = y /\ w = x )
47		elequ1 1759	. . . . . . . . . . . . . 14 |- ( w = x -> ( w e. z <-> x e. z ) )
48	47	adantl 466	. . . . . . . . . . . . 13 |- ( ( -. A. x x = y /\ w = x ) -> ( w e. z <-> x e. z ) )
49	46, 48	albid 1819	. . . . . . . . . . . 12 |- ( ( -. A. x x = y /\ w = x ) -> ( A. y w e. z <-> A. y x e. z ) )
50	49	adantlr 714	. . . . . . . . . . 11 |- ( ( ( -. A. x x = y /\ -. A. x x = z ) /\ w = x ) -> ( A. y w e. z <-> A. y x e. z ) )
51	45, 50	imbi12d 320	. . . . . . . . . 10 |- ( ( ( -. A. x x = y /\ -. A. x x = z ) /\ w = x ) -> ( ( E. z w e. y -> A. y w e. z ) <-> ( E. z x e. y -> A. y x e. z ) ) )
52	51	ex 434	. . . . . . . . 9 |- ( ( -. A. x x = y /\ -. A. x x = z ) -> ( w = x -> ( ( E. z w e. y -> A. y w e. z ) <-> ( E. z x e. y -> A. y x e. z ) ) ) )
53	12, 28, 52	cbvald 1973	. . . . . . . 8 |- ( ( -. A. x x = y /\ -. A. x x = z ) -> ( A. w ( E. z w e. y -> A. y w e. z ) <-> A. x ( E. z x e. y -> A. y x e. z ) ) )
54	53	adantr 465	. . . . . . 7 |- ( ( ( -. A. x x = y /\ -. A. x x = z ) /\ w = x ) -> ( A. w ( E. z w e. y -> A. y w e. z ) <-> A. x ( E. z x e. y -> A. y x e. z ) ) )
55		elequ2 1761	. . . . . . . 8 |- ( w = x -> ( y e. w <-> y e. x ) )
56	55	adantl 466	. . . . . . 7 |- ( ( ( -. A. x x = y /\ -. A. x x = z ) /\ w = x ) -> ( y e. w <-> y e. x ) )
57	54, 56	imbi12d 320	. . . . . 6 |- ( ( ( -. A. x x = y /\ -. A. x x = z ) /\ w = x ) -> ( ( A. w ( E. z w e. y -> A. y w e. z ) -> y e. w ) <-> ( A. x ( E. z x e. y -> A. y x e. z ) -> y e. x ) ) )
58	37, 57	albid 1819	. . . . 5 |- ( ( ( -. A. x x = y /\ -. A. x x = z ) /\ w = x ) -> ( A. y ( A. w ( E. z w e. y -> A. y w e. z ) -> y e. w ) <-> A. y ( A. x ( E. z x e. y -> A. y x e. z ) -> y e. x ) ) )
59	58	ex 434	. . . 4 |- ( ( -. A. x x = y /\ -. A. x x = z ) -> ( w = x -> ( A. y ( A. w ( E. z w e. y -> A. y w e. z ) -> y e. w ) <-> A. y ( A. x ( E. z x e. y -> A. y x e. z ) -> y e. x ) ) ) )
60	12, 33, 59	cbvexd 1974	. . 3 |- ( ( -. A. x x = y /\ -. A. x x = z ) -> ( E. w A. y ( A. w ( E. z w e. y -> A. y w e. z ) -> y e. w ) <-> E. x A. y ( A. x ( E. z x e. y -> A. y x e. z ) -> y e. x ) ) )
61	9, 60	mpbii 211	. 2 |- ( ( -. A. x x = y /\ -. A. x x = z ) -> E. x A. y ( A. x ( E. z x e. y -> A. y x e. z ) -> y e. x ) )
62	61	ex 434	1 |- ( -. A. x x = y -> ( -. A. x x = z -> E. x A. y ( A. x ( E. z x e. y -> A. y x e. z ) -> y e. x ) ) )

Syntax hints:   -. wn 3   -> wi 4   <-> wb 184   /\ wa 369   A.wal 1367   E.wex 1586   F/wnf 1589

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-8 1758  ax-9 1760  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2423  ax-pow 4489

This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1372  df-ex 1587  df-nf 1590  df-cleq 2436  df-clel 2439  df-nfc 2577

This theorem is referenced by:  axpowndlem3  8783