Theorem axpowndlem4 8971

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 8970	. . . . 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 1663	. . . 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 2119	. . . . . 6 |- F/ y -. A. y y = x
4		nfnae 2119	. . . . . 6 |- F/ y -. A. y y = z
5	3, 4	nfan 1988	. . . . 5 |- F/ y ( -. A. y y = x /\ -. A. y y = z )
6		nfcvf 2587	. . . . . . . . 9 |- ( -. A. y y = x -> F/_ y x )
7	6	adantr 466	. . . . . . . 8 |- ( ( -. A. y y = x /\ -. A. y y = z ) -> F/_ y x )
8		nfcvd 2565	. . . . . . . 8 |- ( ( -. A. y y = x /\ -. A. y y = z ) -> F/_ y w )
9	7, 8	nfeqd 2571	. . . . . . 7 |- ( ( -. A. y y = x /\ -. A. y y = z ) -> F/ y x = w )
10	9	nfnd 1961	. . . . . 6 |- ( ( -. A. y y = x /\ -. A. y y = z ) -> F/ y -. x = w )
11		nfnae 2119	. . . . . . . 8 |- F/ x -. A. y y = x
12		nfnae 2119	. . . . . . . 8 |- F/ x -. A. y y = z
13	11, 12	nfan 1988	. . . . . . 7 |- F/ x ( -. A. y y = x /\ -. A. y y = z )
14		nfv 1755	. . . . . . . 8 |- F/ w ( -. A. y y = x /\ -. A. y y = z )
15		nfnae 2119	. . . . . . . . . . . . 13 |- F/ z -. A. y y = x
16		nfnae 2119	. . . . . . . . . . . . 13 |- F/ z -. A. y y = z
17	15, 16	nfan 1988	. . . . . . . . . . . 12 |- F/ z ( -. A. y y = x /\ -. A. y y = z )
18	7, 8	nfeld 2572	. . . . . . . . . . . 12 |- ( ( -. A. y y = x /\ -. A. y y = z ) -> F/ y x e. w )
19	17, 18	nfexd 2012	. . . . . . . . . . 11 |- ( ( -. A. y y = x /\ -. A. y y = z ) -> F/ y E. z x e. w )
20		nfcvf 2587	. . . . . . . . . . . . . 14 |- ( -. A. y y = z -> F/_ y z )
21	20	adantl 467	. . . . . . . . . . . . 13 |- ( ( -. A. y y = x /\ -. A. y y = z ) -> F/_ y z )
22	7, 21	nfeld 2572	. . . . . . . . . . . 12 |- ( ( -. A. y y = x /\ -. A. y y = z ) -> F/ y x e. z )
23	14, 22	nfald 2011	. . . . . . . . . . 11 |- ( ( -. A. y y = x /\ -. A. y y = z ) -> F/ y A. w x e. z )
24	19, 23	nfimd 1977	. . . . . . . . . 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 2011	. . . . . . . . 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 2572	. . . . . . . . 9 |- ( ( -. A. y y = x /\ -. A. y y = z ) -> F/ y w e. x )
27	25, 26	nfimd 1977	. . . . . . . 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 2011	. . . . . . 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 2012	. . . . . 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 1977	. . . . 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 1853	. . . . . . . . 9 |- ( w = y -> ( x = w <-> x = y ) )
32	31	notbid 295	. . . . . . . 8 |- ( w = y -> ( -. x = w <-> -. x = y ) )
33	32	adantl 467	. . . . . . 7 |- ( ( ( -. A. y y = x /\ -. A. y y = z ) /\ w = y ) -> ( -. x = w <-> -. x = y ) )
34		nfcvd 2565	. . . . . . . . . . . . . . 15 |- ( ( -. A. y y = x /\ -. A. y y = z ) -> F/_ x w )
35		nfcvf2 2588	. . . . . . . . . . . . . . . 16 |- ( -. A. y y = x -> F/_ x y )
36	35	adantr 466	. . . . . . . . . . . . . . 15 |- ( ( -. A. y y = x /\ -. A. y y = z ) -> F/_ x y )
37	34, 36	nfeqd 2571	. . . . . . . . . . . . . 14 |- ( ( -. A. y y = x /\ -. A. y y = z ) -> F/ x w = y )
38	13, 37	nfan1 1987	. . . . . . . . . . . . 13 |- F/ x ( ( -. A. y y = x /\ -. A. y y = z ) /\ w = y )
39		nfcvd 2565	. . . . . . . . . . . . . . . . 17 |- ( ( -. A. y y = x /\ -. A. y y = z ) -> F/_ z w )
40		nfcvf2 2588	. . . . . . . . . . . . . . . . . 18 |- ( -. A. y y = z -> F/_ z y )
41	40	adantl 467	. . . . . . . . . . . . . . . . 17 |- ( ( -. A. y y = x /\ -. A. y y = z ) -> F/_ z y )
42	39, 41	nfeqd 2571	. . . . . . . . . . . . . . . 16 |- ( ( -. A. y y = x /\ -. A. y y = z ) -> F/ z w = y )
43	17, 42	nfan1 1987	. . . . . . . . . . . . . . 15 |- F/ z ( ( -. A. y y = x /\ -. A. y y = z ) /\ w = y )
44		elequ2 1877	. . . . . . . . . . . . . . . 16 |- ( w = y -> ( x e. w <-> x e. y ) )
45	44	adantl 467	. . . . . . . . . . . . . . 15 |- ( ( ( -. A. y y = x /\ -. A. y y = z ) /\ w = y ) -> ( x e. w <-> x e. y ) )
46	43, 45	exbid 1941	. . . . . . . . . . . . . 14 |- ( ( ( -. A. y y = x /\ -. A. y y = z ) /\ w = y ) -> ( E. z x e. w <-> E. z x e. y ) )
47		biidd 240	. . . . . . . . . . . . . . . . 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 2085	. . . . . . . . . . . . . . 15 |- ( ( -. A. y y = x /\ -. A. y y = z ) -> ( A. w x e. z <-> A. y x e. z ) )
50	49	adantr 466	. . . . . . . . . . . . . 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 321	. . . . . . . . . . . . 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 1940	. . . . . . . . . . . 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 1875	. . . . . . . . . . . . 13 |- ( w = y -> ( w e. x <-> y e. x ) )
54	53	adantl 467	. . . . . . . . . . . 12 |- ( ( ( -. A. y y = x /\ -. A. y y = z ) /\ w = y ) -> ( w e. x <-> y e. x ) )
55	52, 54	imbi12d 321	. . . . . . . . . . 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 435	. . . . . . . . . 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 2085	. . . . . . . . 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 1941	. . . . . . . 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 466	. . . . . . 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 321	. . . . . 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 435	. . . . 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 2085	. . . 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 214	. . 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 1924	. 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 435	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 187   /\ wa 370   A.wal 1435   E.wex 1657   F/_wnfc 2551

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1663  ax-4 1676  ax-5 1752  ax-6 1798  ax-7 1843  ax-8 1874  ax-9 1876  ax-10 1891  ax-11 1896  ax-12 1909  ax-13 2058  ax-ext 2403  ax-sep 4484  ax-nul 4493  ax-pow 4540  ax-pr 4598  ax-reg 8055

This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-tru 1440  df-ex 1658  df-nf 1662  df-sb 1791  df-clab 2410  df-cleq 2416  df-clel 2419  df-nfc 2553  df-ne 2596  df-ral 2714  df-rex 2715  df-v 3019  df-dif 3377  df-un 3379  df-in 3381  df-ss 3388  df-nul 3700  df-pw 3921  df-sn 3937  df-pr 3939

This theorem is referenced by:  axpownd  8972