Theorem axpowndlem2

Description: Lemma for the Axiom of Power Sets with no distinct variable conditions. Revised to remove a redundant antecedent from the consequence. Usage of this theorem is discouraged because it depends on ax-13 . (Contributed by NM, 4-Jan-2002) (Proof shortened by Mario Carneiro, 6-Dec-2016) (Revised and shortened by Wolf Lammen, 9-Jun-2019.) (New usage is discouraged.)

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

Proof

Step	Hyp	Ref	Expression
1		zfpow	|- E. w A. y ( A. w ( w e. y -> w e. z ) -> y e. w )
2		19.8a	|- ( w e. y -> E. z w e. y )
3		sp	|- ( A. y w e. z -> w e. z )
4	2 3	imim12i	|- ( ( E. z w e. y -> A. y w e. z ) -> ( w e. y -> w e. z ) )
5	4	alimi	|- ( A. w ( E. z w e. y -> A. y w e. z ) -> A. w ( w e. y -> w e. z ) )
6	5	imim1i	|- ( ( A. w ( w e. y -> w e. z ) -> y e. w ) -> ( A. w ( E. z w e. y -> A. y w e. z ) -> y e. w ) )
7	6	alimi	|- ( A. y ( A. w ( w e. y -> w e. z ) -> y e. w ) -> A. y ( A. w ( E. z w e. y -> A. y w e. z ) -> y e. w ) )
8	1 7	eximii	|- E. w A. y ( A. w ( E. z w e. y -> A. y w e. z ) -> y e. w )
9		nfnae	|- F/ x -. A. x x = y
10		nfnae	|- F/ x -. A. x x = z
11	9 10	nfan	|- F/ x ( -. A. x x = y /\ -. A. x x = z )
12		nfnae	|- F/ y -. A. x x = y
13		nfnae	|- F/ y -. A. x x = z
14	12 13	nfan	|- F/ y ( -. A. x x = y /\ -. A. x x = z )
15		nfv	|- F/ w ( -. A. x x = y /\ -. A. x x = z )
16		nfnae	|- F/ z -. A. x x = y
17		nfcvd	|- ( -. A. x x = y -> F/_ x w )
18		nfcvf	|- ( -. A. x x = y -> F/_ x y )
19	17 18	nfeld	|- ( -. A. x x = y -> F/ x w e. y )
20	16 19	nfexd	|- ( -. A. x x = y -> F/ x E. z w e. y )
21	20	adantr	|- ( ( -. A. x x = y /\ -. A. x x = z ) -> F/ x E. z w e. y )
22		nfcvd	|- ( -. A. x x = z -> F/_ x w )
23		nfcvf	|- ( -. A. x x = z -> F/_ x z )
24	22 23	nfeld	|- ( -. A. x x = z -> F/ x w e. z )
25	13 24	nfald	|- ( -. A. x x = z -> F/ x A. y w e. z )
26	25	adantl	|- ( ( -. A. x x = y /\ -. A. x x = z ) -> F/ x A. y w e. z )
27	21 26	nfimd	|- ( ( -. A. x x = y /\ -. A. x x = z ) -> F/ x ( E. z w e. y -> A. y w e. z ) )
28	15 27	nfald	|- ( ( -. A. x x = y /\ -. A. x x = z ) -> F/ x A. w ( E. z w e. y -> A. y w e. z ) )
29	18 17	nfeld	|- ( -. A. x x = y -> F/ x y e. w )
30	29	adantr	|- ( ( -. A. x x = y /\ -. A. x x = z ) -> F/ x y e. w )
31	28 30	nfimd	|- ( ( -. A. x x = y /\ -. A. x x = z ) -> F/ x ( A. w ( E. z w e. y -> A. y w e. z ) -> y e. w ) )
32	14 31	nfald	|- ( ( -. A. x x = y /\ -. A. x x = z ) -> F/ x A. y ( A. w ( E. z w e. y -> A. y w e. z ) -> y e. w ) )
33		nfeqf2	|- ( -. A. y y = x -> F/ y w = x )
34	33	naecoms	|- ( -. A. x x = y -> F/ y w = x )
35	34	adantr	|- ( ( -. A. x x = y /\ -. A. x x = z ) -> F/ y w = x )
36	14 35	nfan1	|- F/ y ( ( -. A. x x = y /\ -. A. x x = z ) /\ w = x )
37		nfnae	|- F/ z -. A. x x = z
38		nfeqf2	|- ( -. A. z z = x -> F/ z w = x )
39	38	naecoms	|- ( -. A. x x = z -> F/ z w = x )
40	37 39	nfan1	|- F/ z ( -. A. x x = z /\ w = x )
41		elequ1	|- ( w = x -> ( w e. y <-> x e. y ) )
42	41	adantl	|- ( ( -. A. x x = z /\ w = x ) -> ( w e. y <-> x e. y ) )
43	40 42	exbid	|- ( ( -. A. x x = z /\ w = x ) -> ( E. z w e. y <-> E. z x e. y ) )
44	43	adantll	|- ( ( ( -. A. x x = y /\ -. A. x x = z ) /\ w = x ) -> ( E. z w e. y <-> E. z x e. y ) )
45	12 34	nfan1	|- F/ y ( -. A. x x = y /\ w = x )
46		elequ1	|- ( w = x -> ( w e. z <-> x e. z ) )
47	46	adantl	|- ( ( -. A. x x = y /\ w = x ) -> ( w e. z <-> x e. z ) )
48	45 47	albid	|- ( ( -. A. x x = y /\ w = x ) -> ( A. y w e. z <-> A. y x e. z ) )
49	48	adantlr	|- ( ( ( -. A. x x = y /\ -. A. x x = z ) /\ w = x ) -> ( A. y w e. z <-> A. y x e. z ) )
50	44 49	imbi12d	|- ( ( ( -. A. x x = y /\ -. A. x x = z ) /\ w = x ) -> ( ( E. z w e. y -> A. y w e. z ) <-> ( E. z x e. y -> A. y x e. z ) ) )
51	50	ex	|- ( ( -. A. x x = y /\ -. A. x x = z ) -> ( w = x -> ( ( E. z w e. y -> A. y w e. z ) <-> ( E. z x e. y -> A. y x e. z ) ) ) )
52	11 27 51	cbvald	|- ( ( -. A. x x = y /\ -. A. x x = z ) -> ( A. w ( E. z w e. y -> A. y w e. z ) <-> A. x ( E. z x e. y -> A. y x e. z ) ) )
53	52	adantr	|- ( ( ( -. A. x x = y /\ -. A. x x = z ) /\ w = x ) -> ( A. w ( E. z w e. y -> A. y w e. z ) <-> A. x ( E. z x e. y -> A. y x e. z ) ) )
54		elequ2	|- ( w = x -> ( y e. w <-> y e. x ) )
55	54	adantl	|- ( ( ( -. A. x x = y /\ -. A. x x = z ) /\ w = x ) -> ( y e. w <-> y e. x ) )
56	53 55	imbi12d	|- ( ( ( -. A. x x = y /\ -. A. x x = z ) /\ w = x ) -> ( ( A. w ( E. z w e. y -> A. y w e. z ) -> y e. w ) <-> ( A. x ( E. z x e. y -> A. y x e. z ) -> y e. x ) ) )
57	36 56	albid	|- ( ( ( -. A. x x = y /\ -. A. x x = z ) /\ w = x ) -> ( A. y ( A. w ( E. z w e. y -> A. y w e. z ) -> y e. w ) <-> A. y ( A. x ( E. z x e. y -> A. y x e. z ) -> y e. x ) ) )
58	57	ex	|- ( ( -. A. x x = y /\ -. A. x x = z ) -> ( w = x -> ( A. y ( A. w ( E. z w e. y -> A. y w e. z ) -> y e. w ) <-> A. y ( A. x ( E. z x e. y -> A. y x e. z ) -> y e. x ) ) ) )
59	11 32 58	cbvexd	|- ( ( -. A. x x = y /\ -. A. x x = z ) -> ( E. w A. y ( A. w ( E. z w e. y -> A. y w e. z ) -> y e. w ) <-> E. x A. y ( A. x ( E. z x e. y -> A. y x e. z ) -> y e. x ) ) )
60	8 59	mpbii	|- ( ( -. A. x x = y /\ -. A. x x = z ) -> E. x A. y ( A. x ( E. z x e. y -> A. y x e. z ) -> y e. x ) )
61	60	ex	|- ( -. A. x x = y -> ( -. A. x x = z -> E. x A. y ( A. x ( E. z x e. y -> A. y x e. z ) -> y e. x ) ) )