Theorem axpowndlem4 9422

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 9421	. . . . 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 1722	. . . 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 2318	. . . . . 6 |- F/ y -. A. y y = x
4		nfnae 2318	. . . . . 6 |- F/ y -. A. y y = z
5	3, 4	nfan 1828	. . . . 5 |- F/ y ( -. A. y y = x /\ -. A. y y = z )
6		nfcvf 2788	. . . . . . . . 9 |- ( -. A. y y = x -> F/_ y x )
7	6	adantr 481	. . . . . . . 8 |- ( ( -. A. y y = x /\ -. A. y y = z ) -> F/_ y x )
8		nfcvd 2765	. . . . . . . 8 |- ( ( -. A. y y = x /\ -. A. y y = z ) -> F/_ y w )
9	7, 8	nfeqd 2772	. . . . . . 7 |- ( ( -. A. y y = x /\ -. A. y y = z ) -> F/ y x = w )
10	9	nfnd 1785	. . . . . 6 |- ( ( -. A. y y = x /\ -. A. y y = z ) -> F/ y -. x = w )
11		nfnae 2318	. . . . . . . 8 |- F/ x -. A. y y = x
12		nfnae 2318	. . . . . . . 8 |- F/ x -. A. y y = z
13	11, 12	nfan 1828	. . . . . . 7 |- F/ x ( -. A. y y = x /\ -. A. y y = z )
14		nfv 1843	. . . . . . . 8 |- F/ w ( -. A. y y = x /\ -. A. y y = z )
15		nfnae 2318	. . . . . . . . . . . . 13 |- F/ z -. A. y y = x
16		nfnae 2318	. . . . . . . . . . . . 13 |- F/ z -. A. y y = z
17	15, 16	nfan 1828	. . . . . . . . . . . 12 |- F/ z ( -. A. y y = x /\ -. A. y y = z )
18	7, 8	nfeld 2773	. . . . . . . . . . . 12 |- ( ( -. A. y y = x /\ -. A. y y = z ) -> F/ y x e. w )
19	17, 18	nfexd 2167	. . . . . . . . . . 11 |- ( ( -. A. y y = x /\ -. A. y y = z ) -> F/ y E. z x e. w )
20		nfcvf 2788	. . . . . . . . . . . . . 14 |- ( -. A. y y = z -> F/_ y z )
21	20	adantl 482	. . . . . . . . . . . . 13 |- ( ( -. A. y y = x /\ -. A. y y = z ) -> F/_ y z )
22	7, 21	nfeld 2773	. . . . . . . . . . . 12 |- ( ( -. A. y y = x /\ -. A. y y = z ) -> F/ y x e. z )
23	14, 22	nfald 2165	. . . . . . . . . . 11 |- ( ( -. A. y y = x /\ -. A. y y = z ) -> F/ y A. w x e. z )
24	19, 23	nfimd 1823	. . . . . . . . . 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 2165	. . . . . . . . 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 2773	. . . . . . . . 9 |- ( ( -. A. y y = x /\ -. A. y y = z ) -> F/ y w e. x )
27	25, 26	nfimd 1823	. . . . . . . 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 2165	. . . . . . 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 2167	. . . . . 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 1823	. . . . 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 1953	. . . . . . . . 9 |- ( w = y -> ( x = w <-> x = y ) )
32	31	notbid 308	. . . . . . . 8 |- ( w = y -> ( -. x = w <-> -. x = y ) )
33	32	adantl 482	. . . . . . 7 |- ( ( ( -. A. y y = x /\ -. A. y y = z ) /\ w = y ) -> ( -. x = w <-> -. x = y ) )
34		nfcvd 2765	. . . . . . . . . . . . . . 15 |- ( ( -. A. y y = x /\ -. A. y y = z ) -> F/_ x w )
35		nfcvf2 2789	. . . . . . . . . . . . . . . 16 |- ( -. A. y y = x -> F/_ x y )
36	35	adantr 481	. . . . . . . . . . . . . . 15 |- ( ( -. A. y y = x /\ -. A. y y = z ) -> F/_ x y )
37	34, 36	nfeqd 2772	. . . . . . . . . . . . . 14 |- ( ( -. A. y y = x /\ -. A. y y = z ) -> F/ x w = y )
38	13, 37	nfan1 2068	. . . . . . . . . . . . 13 |- F/ x ( ( -. A. y y = x /\ -. A. y y = z ) /\ w = y )
39		nfcvd 2765	. . . . . . . . . . . . . . . . 17 |- ( ( -. A. y y = x /\ -. A. y y = z ) -> F/_ z w )
40		nfcvf2 2789	. . . . . . . . . . . . . . . . . 18 |- ( -. A. y y = z -> F/_ z y )
41	40	adantl 482	. . . . . . . . . . . . . . . . 17 |- ( ( -. A. y y = x /\ -. A. y y = z ) -> F/_ z y )
42	39, 41	nfeqd 2772	. . . . . . . . . . . . . . . 16 |- ( ( -. A. y y = x /\ -. A. y y = z ) -> F/ z w = y )
43	17, 42	nfan1 2068	. . . . . . . . . . . . . . 15 |- F/ z ( ( -. A. y y = x /\ -. A. y y = z ) /\ w = y )
44		elequ2 2004	. . . . . . . . . . . . . . . 16 |- ( w = y -> ( x e. w <-> x e. y ) )
45	44	adantl 482	. . . . . . . . . . . . . . 15 |- ( ( ( -. A. y y = x /\ -. A. y y = z ) /\ w = y ) -> ( x e. w <-> x e. y ) )
46	43, 45	exbid 2091	. . . . . . . . . . . . . 14 |- ( ( ( -. A. y y = x /\ -. A. y y = z ) /\ w = y ) -> ( E. z x e. w <-> E. z x e. y ) )
47		biidd 252	. . . . . . . . . . . . . . . . 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 2277	. . . . . . . . . . . . . . 15 |- ( ( -. A. y y = x /\ -. A. y y = z ) -> ( A. w x e. z <-> A. y x e. z ) )
50	49	adantr 481	. . . . . . . . . . . . . 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 334	. . . . . . . . . . . . 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 2090	. . . . . . . . . . . 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 1997	. . . . . . . . . . . . 13 |- ( w = y -> ( w e. x <-> y e. x ) )
54	53	adantl 482	. . . . . . . . . . . 12 |- ( ( ( -. A. y y = x /\ -. A. y y = z ) /\ w = y ) -> ( w e. x <-> y e. x ) )
55	52, 54	imbi12d 334	. . . . . . . . . . 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 450	. . . . . . . . . 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 2277	. . . . . . . . 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 2091	. . . . . . . 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 481	. . . . . . 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 334	. . . . . 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 450	. . . . 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 2277	. . . 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 223	. . 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 2059	. 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 450	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 196   /\ wa 384   A.wal 1481   E.wex 1704   F/_wnfc 2751

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-8 1992  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602  ax-sep 4781  ax-nul 4789  ax-pow 4843  ax-pr 4906  ax-reg 8497

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-ral 2917  df-rex 2918  df-v 3202  df-dif 3577  df-un 3579  df-in 3581  df-ss 3588  df-nul 3916  df-pw 4160  df-sn 4178  df-pr 4180

This theorem is referenced by:  axpownd  9423