Theorem axpowndlem4 8966

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 8965	. . . . 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 1623	. . . 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 2062	. . . . . 6 |- F/ y -. A. y y = x
4		nfnae 2062	. . . . . 6 |- F/ y -. A. y y = z
5	3, 4	nfan 1933	. . . . 5 |- F/ y ( -. A. y y = x /\ -. A. y y = z )
6		nfcvf 2641	. . . . . . . . 9 |- ( -. A. y y = x -> F/_ y x )
7	6	adantr 463	. . . . . . . 8 |- ( ( -. A. y y = x /\ -. A. y y = z ) -> F/_ y x )
8		nfcvd 2617	. . . . . . . 8 |- ( ( -. A. y y = x /\ -. A. y y = z ) -> F/_ y w )
9	7, 8	nfeqd 2623	. . . . . . 7 |- ( ( -. A. y y = x /\ -. A. y y = z ) -> F/ y x = w )
10	9	nfnd 1907	. . . . . 6 |- ( ( -. A. y y = x /\ -. A. y y = z ) -> F/ y -. x = w )
11		nfnae 2062	. . . . . . . 8 |- F/ x -. A. y y = x
12		nfnae 2062	. . . . . . . 8 |- F/ x -. A. y y = z
13	11, 12	nfan 1933	. . . . . . 7 |- F/ x ( -. A. y y = x /\ -. A. y y = z )
14		nfv 1712	. . . . . . . 8 |- F/ w ( -. A. y y = x /\ -. A. y y = z )
15		nfnae 2062	. . . . . . . . . . . . 13 |- F/ z -. A. y y = x
16		nfnae 2062	. . . . . . . . . . . . 13 |- F/ z -. A. y y = z
17	15, 16	nfan 1933	. . . . . . . . . . . 12 |- F/ z ( -. A. y y = x /\ -. A. y y = z )
18	7, 8	nfeld 2624	. . . . . . . . . . . 12 |- ( ( -. A. y y = x /\ -. A. y y = z ) -> F/ y x e. w )
19	17, 18	nfexd 1957	. . . . . . . . . . 11 |- ( ( -. A. y y = x /\ -. A. y y = z ) -> F/ y E. z x e. w )
20		nfcvf 2641	. . . . . . . . . . . . . 14 |- ( -. A. y y = z -> F/_ y z )
21	20	adantl 464	. . . . . . . . . . . . 13 |- ( ( -. A. y y = x /\ -. A. y y = z ) -> F/_ y z )
22	7, 21	nfeld 2624	. . . . . . . . . . . 12 |- ( ( -. A. y y = x /\ -. A. y y = z ) -> F/ y x e. z )
23	14, 22	nfald 1956	. . . . . . . . . . 11 |- ( ( -. A. y y = x /\ -. A. y y = z ) -> F/ y A. w x e. z )
24	19, 23	nfimd 1922	. . . . . . . . . 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 1956	. . . . . . . . 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 2624	. . . . . . . . 9 |- ( ( -. A. y y = x /\ -. A. y y = z ) -> F/ y w e. x )
27	25, 26	nfimd 1922	. . . . . . . 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 1956	. . . . . . 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 1957	. . . . . 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 1922	. . . . 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 1804	. . . . . . . . 9 |- ( w = y -> ( x = w <-> x = y ) )
32	31	notbid 292	. . . . . . . 8 |- ( w = y -> ( -. x = w <-> -. x = y ) )
33	32	adantl 464	. . . . . . 7 |- ( ( ( -. A. y y = x /\ -. A. y y = z ) /\ w = y ) -> ( -. x = w <-> -. x = y ) )
34		nfcvd 2617	. . . . . . . . . . . . . . 15 |- ( ( -. A. y y = x /\ -. A. y y = z ) -> F/_ x w )
35		nfcvf2 2642	. . . . . . . . . . . . . . . 16 |- ( -. A. y y = x -> F/_ x y )
36	35	adantr 463	. . . . . . . . . . . . . . 15 |- ( ( -. A. y y = x /\ -. A. y y = z ) -> F/_ x y )
37	34, 36	nfeqd 2623	. . . . . . . . . . . . . 14 |- ( ( -. A. y y = x /\ -. A. y y = z ) -> F/ x w = y )
38	13, 37	nfan1 1932	. . . . . . . . . . . . 13 |- F/ x ( ( -. A. y y = x /\ -. A. y y = z ) /\ w = y )
39		nfcvd 2617	. . . . . . . . . . . . . . . . 17 |- ( ( -. A. y y = x /\ -. A. y y = z ) -> F/_ z w )
40		nfcvf2 2642	. . . . . . . . . . . . . . . . . 18 |- ( -. A. y y = z -> F/_ z y )
41	40	adantl 464	. . . . . . . . . . . . . . . . 17 |- ( ( -. A. y y = x /\ -. A. y y = z ) -> F/_ z y )
42	39, 41	nfeqd 2623	. . . . . . . . . . . . . . . 16 |- ( ( -. A. y y = x /\ -. A. y y = z ) -> F/ z w = y )
43	17, 42	nfan1 1932	. . . . . . . . . . . . . . 15 |- F/ z ( ( -. A. y y = x /\ -. A. y y = z ) /\ w = y )
44		elequ2 1828	. . . . . . . . . . . . . . . 16 |- ( w = y -> ( x e. w <-> x e. y ) )
45	44	adantl 464	. . . . . . . . . . . . . . 15 |- ( ( ( -. A. y y = x /\ -. A. y y = z ) /\ w = y ) -> ( x e. w <-> x e. y ) )
46	43, 45	exbid 1891	. . . . . . . . . . . . . 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 2030	. . . . . . . . . . . . . . 15 |- ( ( -. A. y y = x /\ -. A. y y = z ) -> ( A. w x e. z <-> A. y x e. z ) )
50	49	adantr 463	. . . . . . . . . . . . . 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 318	. . . . . . . . . . . . 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 1890	. . . . . . . . . . . 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 1826	. . . . . . . . . . . . 13 |- ( w = y -> ( w e. x <-> y e. x ) )
54	53	adantl 464	. . . . . . . . . . . 12 |- ( ( ( -. A. y y = x /\ -. A. y y = z ) /\ w = y ) -> ( w e. x <-> y e. x ) )
55	52, 54	imbi12d 318	. . . . . . . . . . 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 432	. . . . . . . . . 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 2030	. . . . . . . . 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 1891	. . . . . . . 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 463	. . . . . . 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 318	. . . . . 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 432	. . . . 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 2030	. . . 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 1874	. 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 432	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 367   A.wal 1396   E.wex 1617   F/_wnfc 2602

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1623  ax-4 1636  ax-5 1709  ax-6 1752  ax-7 1795  ax-8 1825  ax-9 1827  ax-10 1842  ax-11 1847  ax-12 1859  ax-13 2004  ax-ext 2432  ax-sep 4560  ax-nul 4568  ax-pow 4615  ax-pr 4676  ax-reg 8010

This theorem depends on definitions:  df-bi 185  df-or 368  df-an 369  df-tru 1401  df-ex 1618  df-nf 1622  df-sb 1745  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2604  df-ne 2651  df-ral 2809  df-rex 2810  df-v 3108  df-dif 3464  df-un 3466  df-in 3468  df-ss 3475  df-nul 3784  df-pw 4001  df-sn 4017  df-pr 4019

This theorem is referenced by:  axpownd  8967