Metamath Proof Explorer


Theorem axpowndlem3

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

Ref Expression
Assertion axpowndlem3
|- ( -. x = y -> 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 sp
 |-  ( A. x x = y -> x = y )
2 p0ex
 |-  { (/) } e. _V
3 eleq2
 |-  ( x = { (/) } -> ( w e. x <-> w e. { (/) } ) )
4 3 imbi2d
 |-  ( x = { (/) } -> ( ( w = (/) -> w e. x ) <-> ( w = (/) -> w e. { (/) } ) ) )
5 4 albidv
 |-  ( x = { (/) } -> ( A. w ( w = (/) -> w e. x ) <-> A. w ( w = (/) -> w e. { (/) } ) ) )
6 2 5 spcev
 |-  ( A. w ( w = (/) -> w e. { (/) } ) -> E. x A. w ( w = (/) -> w e. x ) )
7 0ex
 |-  (/) e. _V
8 7 snid
 |-  (/) e. { (/) }
9 eleq1
 |-  ( w = (/) -> ( w e. { (/) } <-> (/) e. { (/) } ) )
10 8 9 mpbiri
 |-  ( w = (/) -> w e. { (/) } )
11 6 10 mpg
 |-  E. x A. w ( w = (/) -> w e. x )
12 neq0
 |-  ( -. w = (/) <-> E. x x e. w )
13 12 con1bii
 |-  ( -. E. x x e. w <-> w = (/) )
14 13 imbi1i
 |-  ( ( -. E. x x e. w -> w e. x ) <-> ( w = (/) -> w e. x ) )
15 14 albii
 |-  ( A. w ( -. E. x x e. w -> w e. x ) <-> A. w ( w = (/) -> w e. x ) )
16 15 exbii
 |-  ( E. x A. w ( -. E. x x e. w -> w e. x ) <-> E. x A. w ( w = (/) -> w e. x ) )
17 11 16 mpbir
 |-  E. x A. w ( -. E. x x e. w -> w e. x )
18 nfnae
 |-  F/ x -. A. x x = y
19 nfnae
 |-  F/ y -. A. x x = y
20 nfcvf2
 |-  ( -. A. x x = y -> F/_ y x )
21 nfcvd
 |-  ( -. A. x x = y -> F/_ y w )
22 20 21 nfeld
 |-  ( -. A. x x = y -> F/ y x e. w )
23 18 22 nfexd
 |-  ( -. A. x x = y -> F/ y E. x x e. w )
24 23 nfnd
 |-  ( -. A. x x = y -> F/ y -. E. x x e. w )
25 21 20 nfeld
 |-  ( -. A. x x = y -> F/ y w e. x )
26 24 25 nfimd
 |-  ( -. A. x x = y -> F/ y ( -. E. x x e. w -> w e. x ) )
27 nfeqf2
 |-  ( -. A. x x = y -> F/ x w = y )
28 18 27 nfan1
 |-  F/ x ( -. A. x x = y /\ w = y )
29 elequ2
 |-  ( w = y -> ( x e. w <-> x e. y ) )
30 29 adantl
 |-  ( ( -. A. x x = y /\ w = y ) -> ( x e. w <-> x e. y ) )
31 28 30 exbid
 |-  ( ( -. A. x x = y /\ w = y ) -> ( E. x x e. w <-> E. x x e. y ) )
32 31 notbid
 |-  ( ( -. A. x x = y /\ w = y ) -> ( -. E. x x e. w <-> -. E. x x e. y ) )
33 elequ1
 |-  ( w = y -> ( w e. x <-> y e. x ) )
34 33 adantl
 |-  ( ( -. A. x x = y /\ w = y ) -> ( w e. x <-> y e. x ) )
35 32 34 imbi12d
 |-  ( ( -. A. x x = y /\ w = y ) -> ( ( -. E. x x e. w -> w e. x ) <-> ( -. E. x x e. y -> y e. x ) ) )
36 35 ex
 |-  ( -. A. x x = y -> ( w = y -> ( ( -. E. x x e. w -> w e. x ) <-> ( -. E. x x e. y -> y e. x ) ) ) )
37 19 26 36 cbvald
 |-  ( -. A. x x = y -> ( A. w ( -. E. x x e. w -> w e. x ) <-> A. y ( -. E. x x e. y -> y e. x ) ) )
38 18 37 exbid
 |-  ( -. A. x x = y -> ( E. x A. w ( -. E. x x e. w -> w e. x ) <-> E. x A. y ( -. E. x x e. y -> y e. x ) ) )
39 17 38 mpbii
 |-  ( -. A. x x = y -> E. x A. y ( -. E. x x e. y -> y e. x ) )
40 nfae
 |-  F/ x A. x x = z
41 nfae
 |-  F/ y A. x x = z
42 axc11r
 |-  ( A. x x = z -> ( A. z -. x e. y -> A. x -. x e. y ) )
43 alnex
 |-  ( A. z -. x e. y <-> -. E. z x e. y )
44 alnex
 |-  ( A. x -. x e. y <-> -. E. x x e. y )
45 42 43 44 3imtr3g
 |-  ( A. x x = z -> ( -. E. z x e. y -> -. E. x x e. y ) )
46 nd3
 |-  ( A. x x = z -> -. A. y x e. z )
47 46 pm2.21d
 |-  ( A. x x = z -> ( A. y x e. z -> -. E. x x e. y ) )
48 45 47 jad
 |-  ( A. x x = z -> ( ( E. z x e. y -> A. y x e. z ) -> -. E. x x e. y ) )
49 48 spsd
 |-  ( A. x x = z -> ( A. x ( E. z x e. y -> A. y x e. z ) -> -. E. x x e. y ) )
50 49 imim1d
 |-  ( A. x x = z -> ( ( -. E. x x e. y -> y e. x ) -> ( A. x ( E. z x e. y -> A. y x e. z ) -> y e. x ) ) )
51 41 50 alimd
 |-  ( A. x x = z -> ( A. y ( -. E. x x e. y -> y e. x ) -> A. y ( A. x ( E. z x e. y -> A. y x e. z ) -> y e. x ) ) )
52 40 51 eximd
 |-  ( A. x x = z -> ( E. x A. y ( -. E. x x e. y -> y e. x ) -> E. x A. y ( A. x ( E. z x e. y -> A. y x e. z ) -> y e. x ) ) )
53 39 52 syl5com
 |-  ( -. 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 ) ) )
54 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 ) ) )
55 53 54 pm2.61d
 |-  ( -. A. x x = y -> E. x A. y ( A. x ( E. z x e. y -> A. y x e. z ) -> y e. x ) )
56 1 55 nsyl5
 |-  ( -. x = y -> E. x A. y ( A. x ( E. z x e. y -> A. y x e. z ) -> y e. x ) )