Theorem axpowndlem4 8978

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 8976	. . . . 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 1601	. . . 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 2031	. . . . . 6 |- F/ y -. A. y y = x
4		nfnae 2031	. . . . . 6 |- F/ y -. A. y y = z
5	3, 4	nfan 1875	. . . . 5 |- F/ y ( -. A. y y = x /\ -. A. y y = z )
6		nfcvf 2654	. . . . . . . . 9 |- ( -. A. y y = x -> F/_ y x )
7	6	adantr 465	. . . . . . . 8 |- ( ( -. A. y y = x /\ -. A. y y = z ) -> F/_ y x )
8		nfcvd 2630	. . . . . . . 8 |- ( ( -. A. y y = x /\ -. A. y y = z ) -> F/_ y w )
9	7, 8	nfeqd 2636	. . . . . . 7 |- ( ( -. A. y y = x /\ -. A. y y = z ) -> F/ y x = w )
10	9	nfnd 1850	. . . . . 6 |- ( ( -. A. y y = x /\ -. A. y y = z ) -> F/ y -. x = w )
11		nfnae 2031	. . . . . . . 8 |- F/ x -. A. y y = x
12		nfnae 2031	. . . . . . . 8 |- F/ x -. A. y y = z
13	11, 12	nfan 1875	. . . . . . 7 |- F/ x ( -. A. y y = x /\ -. A. y y = z )
14		nfv 1683	. . . . . . . 8 |- F/ w ( -. A. y y = x /\ -. A. y y = z )
15		nfnae 2031	. . . . . . . . . . . . 13 |- F/ z -. A. y y = x
16		nfnae 2031	. . . . . . . . . . . . 13 |- F/ z -. A. y y = z
17	15, 16	nfan 1875	. . . . . . . . . . . 12 |- F/ z ( -. A. y y = x /\ -. A. y y = z )
18	7, 8	nfeld 2637	. . . . . . . . . . . 12 |- ( ( -. A. y y = x /\ -. A. y y = z ) -> F/ y x e. w )
19	17, 18	nfexd 1899	. . . . . . . . . . 11 |- ( ( -. A. y y = x /\ -. A. y y = z ) -> F/ y E. z x e. w )
20		nfcvf 2654	. . . . . . . . . . . . . 14 |- ( -. A. y y = z -> F/_ y z )
21	20	adantl 466	. . . . . . . . . . . . 13 |- ( ( -. A. y y = x /\ -. A. y y = z ) -> F/_ y z )
22	7, 21	nfeld 2637	. . . . . . . . . . . 12 |- ( ( -. A. y y = x /\ -. A. y y = z ) -> F/ y x e. z )
23	14, 22	nfald 1898	. . . . . . . . . . 11 |- ( ( -. A. y y = x /\ -. A. y y = z ) -> F/ y A. w x e. z )
24	19, 23	nfimd 1864	. . . . . . . . . 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 1898	. . . . . . . . 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 2637	. . . . . . . . 9 |- ( ( -. A. y y = x /\ -. A. y y = z ) -> F/ y w e. x )
27	25, 26	nfimd 1864	. . . . . . . 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 1898	. . . . . . 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 1899	. . . . . 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 1864	. . . . 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 1748	. . . . . . . . 9 |- ( w = y -> ( x = w <-> x = y ) )
32	31	notbid 294	. . . . . . . 8 |- ( w = y -> ( -. x = w <-> -. x = y ) )
33	32	adantl 466	. . . . . . 7 |- ( ( ( -. A. y y = x /\ -. A. y y = z ) /\ w = y ) -> ( -. x = w <-> -. x = y ) )
34		nfcvd 2630	. . . . . . . . . . . . . . 15 |- ( ( -. A. y y = x /\ -. A. y y = z ) -> F/_ x w )
35		nfcvf2 2655	. . . . . . . . . . . . . . . 16 |- ( -. A. y y = x -> F/_ x y )
36	35	adantr 465	. . . . . . . . . . . . . . 15 |- ( ( -. A. y y = x /\ -. A. y y = z ) -> F/_ x y )
37	34, 36	nfeqd 2636	. . . . . . . . . . . . . 14 |- ( ( -. A. y y = x /\ -. A. y y = z ) -> F/ x w = y )
38	13, 37	nfan1 1874	. . . . . . . . . . . . 13 |- F/ x ( ( -. A. y y = x /\ -. A. y y = z ) /\ w = y )
39		nfcvd 2630	. . . . . . . . . . . . . . . . 17 |- ( ( -. A. y y = x /\ -. A. y y = z ) -> F/_ z w )
40		nfcvf2 2655	. . . . . . . . . . . . . . . . . 18 |- ( -. A. y y = z -> F/_ z y )
41	40	adantl 466	. . . . . . . . . . . . . . . . 17 |- ( ( -. A. y y = x /\ -. A. y y = z ) -> F/_ z y )
42	39, 41	nfeqd 2636	. . . . . . . . . . . . . . . 16 |- ( ( -. A. y y = x /\ -. A. y y = z ) -> F/ z w = y )
43	17, 42	nfan1 1874	. . . . . . . . . . . . . . 15 |- F/ z ( ( -. A. y y = x /\ -. A. y y = z ) /\ w = y )
44		elequ2 1772	. . . . . . . . . . . . . . . 16 |- ( w = y -> ( x e. w <-> x e. y ) )
45	44	adantl 466	. . . . . . . . . . . . . . 15 |- ( ( ( -. A. y y = x /\ -. A. y y = z ) /\ w = y ) -> ( x e. w <-> x e. y ) )
46	43, 45	exbid 1834	. . . . . . . . . . . . . 14 |- ( ( ( -. A. y y = x /\ -. A. y y = z ) /\ w = y ) -> ( E. z x e. w <-> E. z x e. y ) )
47		biidd 237	. . . . . . . . . . . . . . . . 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 1998	. . . . . . . . . . . . . . 15 |- ( ( -. A. y y = x /\ -. A. y y = z ) -> ( A. w x e. z <-> A. y x e. z ) )
50	49	adantr 465	. . . . . . . . . . . . . 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 320	. . . . . . . . . . . . 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 1833	. . . . . . . . . . . 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 1770	. . . . . . . . . . . . 13 |- ( w = y -> ( w e. x <-> y e. x ) )
54	53	adantl 466	. . . . . . . . . . . 12 |- ( ( ( -. A. y y = x /\ -. A. y y = z ) /\ w = y ) -> ( w e. x <-> y e. x ) )
55	52, 54	imbi12d 320	. . . . . . . . . . 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 434	. . . . . . . . . 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 1998	. . . . . . . . 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 1834	. . . . . . . 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 465	. . . . . . 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 320	. . . . . 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 434	. . . . 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 1998	. . . 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 211	. . 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 1818	. 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 434	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 184   /\ wa 369   A.wal 1377   E.wex 1596   F/_wnfc 2615

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-8 1769  ax-9 1771  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445  ax-sep 4568  ax-nul 4576  ax-pow 4625  ax-pr 4686  ax-reg 8019

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-clab 2453  df-cleq 2459  df-clel 2462  df-nfc 2617  df-ne 2664  df-ral 2819  df-rex 2820  df-v 3115  df-dif 3479  df-un 3481  df-in 3483  df-ss 3490  df-nul 3786  df-pw 4012  df-sn 4028  df-pr 4030

This theorem is referenced by:  axpownd  8979