Metamath Proof Explorer


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 ) ) )