This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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