Theorem axpowndlem4 9050

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

Assertion

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

Proof of Theorem axpowndlem4

Dummy variable w is distinct from all other variables.

Step	Hyp	Ref	Expression
1		axpowndlem3 9049	. . . . 5 |- ( -. x = w -> E. x A. w ( A. x ( E. z x e. w -> A. w x e. z ) -> w e. x ) )
2	1	ax-gen 1679	. . . 4 |- A. w ( -. x = w -> E. x A. w ( A. x ( E. z x e. w -> A. w x e. z ) -> w e. x ) )
3		nfnae 2162	. . . . . 6 |- F/ y -. A. y y = x
4		nfnae 2162	. . . . . 6 |- F/ y -. A. y y = z
5	3, 4	nfan 2021	. . . . 5 |- F/ y ( -. A. y y = x /\ -. A. y y = z )
6		nfcvf 2625	. . . . . . . . 9 |- ( -. A. y y = x -> F/_ y x )
7	6	adantr 471	. . . . . . . 8 |- ( ( -. A. y y = x /\ -. A. y y = z ) -> F/_ y x )
8		nfcvd 2603	. . . . . . . 8 |- ( ( -. A. y y = x /\ -. A. y y = z ) -> F/_ y w )
9	7, 8	nfeqd 2609	. . . . . . 7 |- ( ( -. A. y y = x /\ -. A. y y = z ) -> F/ y x = w )
10	9	nfnd 1994	. . . . . 6 |- ( ( -. A. y y = x /\ -. A. y y = z ) -> F/ y -. x = w )
11		nfnae 2162	. . . . . . . 8 |- F/ x -. A. y y = x
12		nfnae 2162	. . . . . . . 8 |- F/ x -. A. y y = z
13	11, 12	nfan 2021	. . . . . . 7 |- F/ x ( -. A. y y = x /\ -. A. y y = z )
14		nfv 1771	. . . . . . . 8 |- F/ w ( -. A. y y = x /\ -. A. y y = z )
15		nfnae 2162	. . . . . . . . . . . . 13 |- F/ z -. A. y y = x
16		nfnae 2162	. . . . . . . . . . . . 13 |- F/ z -. A. y y = z
17	15, 16	nfan 2021	. . . . . . . . . . . 12 |- F/ z ( -. A. y y = x /\ -. A. y y = z )
18	7, 8	nfeld 2610	. . . . . . . . . . . 12 |- ( ( -. A. y y = x /\ -. A. y y = z ) -> F/ y x e. w )
19	17, 18	nfexd 2045	. . . . . . . . . . 11 |- ( ( -. A. y y = x /\ -. A. y y = z ) -> F/ y E. z x e. w )
20		nfcvf 2625	. . . . . . . . . . . . . 14 |- ( -. A. y y = z -> F/_ y z )
21	20	adantl 472	. . . . . . . . . . . . 13 |- ( ( -. A. y y = x /\ -. A. y y = z ) -> F/_ y z )
22	7, 21	nfeld 2610	. . . . . . . . . . . 12 |- ( ( -. A. y y = x /\ -. A. y y = z ) -> F/ y x e. z )
23	14, 22	nfald 2044	. . . . . . . . . . 11 |- ( ( -. A. y y = x /\ -. A. y y = z ) -> F/ y A. w x e. z )
24	19, 23	nfimd 2010	. . . . . . . . . 10 |- ( ( -. A. y y = x /\ -. A. y y = z ) -> F/ y ( E. z x e. w -> A. w x e. z ) )
25	13, 24	nfald 2044	. . . . . . . . 9 |- ( ( -. A. y y = x /\ -. A. y y = z ) -> F/ y A. x ( E. z x e. w -> A. w x e. z ) )
26	8, 7	nfeld 2610	. . . . . . . . 9 |- ( ( -. A. y y = x /\ -. A. y y = z ) -> F/ y w e. x )
27	25, 26	nfimd 2010	. . . . . . . 8 |- ( ( -. A. y y = x /\ -. A. y y = z ) -> F/ y ( A. x ( E. z x e. w -> A. w x e. z ) -> w e. x ) )
28	14, 27	nfald 2044	. . . . . . 7 |- ( ( -. A. y y = x /\ -. A. y y = z ) -> F/ y A. w ( A. x ( E. z x e. w -> A. w x e. z ) -> w e. x ) )
29	13, 28	nfexd 2045	. . . . . 6 |- ( ( -. A. y y = x /\ -. A. y y = z ) -> F/ y E. x A. w ( A. x ( E. z x e. w -> A. w x e. z ) -> w e. x ) )
30	10, 29	nfimd 2010	. . . . 5 |- ( ( -. A. y y = x /\ -. A. y y = z ) -> F/ y ( -. x = w -> E. x A. w ( A. x ( E. z x e. w -> A. w x e. z ) -> w e. x ) ) )
31		equequ2 1878	. . . . . . . . 9 |- ( w = y -> ( x = w <-> x = y ) )
32	31	notbid 300	. . . . . . . 8 |- ( w = y -> ( -. x = w <-> -. x = y ) )
33	32	adantl 472	. . . . . . 7 |- ( ( ( -. A. y y = x /\ -. A. y y = z ) /\ w = y ) -> ( -. x = w <-> -. x = y ) )
34		nfcvd 2603	. . . . . . . . . . . . . . 15 |- ( ( -. A. y y = x /\ -. A. y y = z ) -> F/_ x w )
35		nfcvf2 2626	. . . . . . . . . . . . . . . 16 |- ( -. A. y y = x -> F/_ x y )
36	35	adantr 471	. . . . . . . . . . . . . . 15 |- ( ( -. A. y y = x /\ -. A. y y = z ) -> F/_ x y )
37	34, 36	nfeqd 2609	. . . . . . . . . . . . . 14 |- ( ( -. A. y y = x /\ -. A. y y = z ) -> F/ x w = y )
38	13, 37	nfan1 2020	. . . . . . . . . . . . 13 |- F/ x ( ( -. A. y y = x /\ -. A. y y = z ) /\ w = y )
39		nfcvd 2603	. . . . . . . . . . . . . . . . 17 |- ( ( -. A. y y = x /\ -. A. y y = z ) -> F/_ z w )
40		nfcvf2 2626	. . . . . . . . . . . . . . . . . 18 |- ( -. A. y y = z -> F/_ z y )
41	40	adantl 472	. . . . . . . . . . . . . . . . 17 |- ( ( -. A. y y = x /\ -. A. y y = z ) -> F/_ z y )
42	39, 41	nfeqd 2609	. . . . . . . . . . . . . . . 16 |- ( ( -. A. y y = x /\ -. A. y y = z ) -> F/ z w = y )
43	17, 42	nfan1 2020	. . . . . . . . . . . . . . 15 |- F/ z ( ( -. A. y y = x /\ -. A. y y = z ) /\ w = y )
44		elequ2 1911	. . . . . . . . . . . . . . . 16 |- ( w = y -> ( x e. w <-> x e. y ) )
45	44	adantl 472	. . . . . . . . . . . . . . 15 |- ( ( ( -. A. y y = x /\ -. A. y y = z ) /\ w = y ) -> ( x e. w <-> x e. y ) )
46	43, 45	exbid 1974	. . . . . . . . . . . . . 14 |- ( ( ( -. A. y y = x /\ -. A. y y = z ) /\ w = y ) -> ( E. z x e. w <-> E. z x e. y ) )
47		biidd 245	. . . . . . . . . . . . . . . . 17 |- ( w = y -> ( x e. z <-> x e. z ) )
48	47	a1i 11	. . . . . . . . . . . . . . . 16 |- ( ( -. A. y y = x /\ -. A. y y = z ) -> ( w = y -> ( x e. z <-> x e. z ) ) )
49	5, 22, 48	cbvald 2128	. . . . . . . . . . . . . . 15 |- ( ( -. A. y y = x /\ -. A. y y = z ) -> ( A. w x e. z <-> A. y x e. z ) )
50	49	adantr 471	. . . . . . . . . . . . . 14 |- ( ( ( -. A. y y = x /\ -. A. y y = z ) /\ w = y ) -> ( A. w x e. z <-> A. y x e. z ) )
51	46, 50	imbi12d 326	. . . . . . . . . . . . 13 |- ( ( ( -. A. y y = x /\ -. A. y y = z ) /\ w = y ) -> ( ( E. z x e. w -> A. w x e. z ) <-> ( E. z x e. y -> A. y x e. z ) ) )
52	38, 51	albid 1973	. . . . . . . . . . . 12 |- ( ( ( -. A. y y = x /\ -. A. y y = z ) /\ w = y ) -> ( A. x ( E. z x e. w -> A. w x e. z ) <-> A. x ( E. z x e. y -> A. y x e. z ) ) )
53		elequ1 1904	. . . . . . . . . . . . 13 |- ( w = y -> ( w e. x <-> y e. x ) )
54	53	adantl 472	. . . . . . . . . . . 12 |- ( ( ( -. A. y y = x /\ -. A. y y = z ) /\ w = y ) -> ( w e. x <-> y e. x ) )
55	52, 54	imbi12d 326	. . . . . . . . . . 11 |- ( ( ( -. A. y y = x /\ -. A. y y = z ) /\ w = y ) -> ( ( A. x ( E. z x e. w -> A. w x e. z ) -> w e. x ) <-> ( A. x ( E. z x e. y -> A. y x e. z ) -> y e. x ) ) )
56	55	ex 440	. . . . . . . . . 10 |- ( ( -. A. y y = x /\ -. A. y y = z ) -> ( w = y -> ( ( A. x ( E. z x e. w -> A. w x e. z ) -> w e. x ) <-> ( A. x ( E. z x e. y -> A. y x e. z ) -> y e. x ) ) ) )
57	5, 27, 56	cbvald 2128	. . . . . . . . 9 |- ( ( -. A. y y = x /\ -. A. y y = z ) -> ( A. w ( A. x ( E. z x e. w -> A. w x e. z ) -> w e. x ) <-> A. y ( A. x ( E. z x e. y -> A. y x e. z ) -> y e. x ) ) )
58	13, 57	exbid 1974	. . . . . . . 8 |- ( ( -. A. y y = x /\ -. A. y y = z ) -> ( E. x A. w ( A. x ( E. z x e. w -> A. w x e. z ) -> w e. x ) <-> E. x A. y ( A. x ( E. z x e. y -> A. y x e. z ) -> y e. x ) ) )
59	58	adantr 471	. . . . . . 7 |- ( ( ( -. A. y y = x /\ -. A. y y = z ) /\ w = y ) -> ( E. x A. w ( A. x ( E. z x e. w -> A. w x e. z ) -> w e. x ) <-> E. x A. y ( A. x ( E. z x e. y -> A. y x e. z ) -> y e. x ) ) )
60	33, 59	imbi12d 326	. . . . . 6 |- ( ( ( -. A. y y = x /\ -. A. y y = z ) /\ w = y ) -> ( ( -. x = w -> E. x A. w ( A. x ( E. z x e. w -> A. w x e. z ) -> w e. x ) ) <-> ( -. x = y -> E. x A. y ( A. x ( E. z x e. y -> A. y x e. z ) -> y e. x ) ) ) )
61	60	ex 440	. . . . 5 |- ( ( -. A. y y = x /\ -. A. y y = z ) -> ( w = y -> ( ( -. x = w -> E. x A. w ( A. x ( E. z x e. w -> A. w x e. z ) -> w e. x ) ) <-> ( -. x = y -> E. x A. y ( A. x ( E. z x e. y -> A. y x e. z ) -> y e. x ) ) ) ) )
62	5, 30, 61	cbvald 2128	. . . 4 |- ( ( -. A. y y = x /\ -. A. y y = z ) -> ( A. w ( -. x = w -> E. x A. w ( A. x ( E. z x e. w -> A. w x e. z ) -> w e. x ) ) <-> A. y ( -. x = y -> E. x A. y ( A. x ( E. z x e. y -> A. y x e. z ) -> y e. x ) ) ) )
63	2, 62	mpbii 216	. . 3 |- ( ( -. A. y y = x /\ -. A. y y = z ) -> A. y ( -. x = y -> E. x A. y ( A. x ( E. z x e. y -> A. y x e. z ) -> y e. x ) ) )
64	63	19.21bi 1957	. 2 |- ( ( -. A. y y = x /\ -. A. y y = z ) -> ( -. x = y -> E. x A. y ( A. x ( E. z x e. y -> A. y x e. z ) -> y e. x ) ) )
65	64	ex 440	1 |- ( -. A. y y = x -> ( -. A. y y = z -> ( -. x = y -> 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 189   /\ wa 375   A.wal 1452   E.wex 1673   F/_wnfc 2589

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1679  ax-4 1692  ax-5 1768  ax-6 1815  ax-7 1861  ax-8 1899  ax-9 1906  ax-10 1925  ax-11 1930  ax-12 1943  ax-13 2101  ax-ext 2441  ax-sep 4538  ax-nul 4547  ax-pow 4594  ax-pr 4652  ax-reg 8132

This theorem depends on definitions:  df-bi 190  df-or 376  df-an 377  df-tru 1457  df-ex 1674  df-nf 1678  df-sb 1808  df-clab 2448  df-cleq 2454  df-clel 2457  df-nfc 2591  df-ne 2634  df-ral 2753  df-rex 2754  df-v 3058  df-dif 3418  df-un 3420  df-in 3422  df-ss 3429  df-nul 3743  df-pw 3964  df-sn 3980  df-pr 3982

This theorem is referenced by:  axpownd  9051