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

Metamath Proof Explorer

Theorem axpownd

Description: A version of 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) (New usage is discouraged.)

Ref Expression
Assertion axpownd 
|- ( -. 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 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 ) ) ) )
2 axpowndlem1 
 |-  ( A. x x = y -> ( -. x = y -> E. x A. y ( A. x ( E. z x e. y -> A. y x e. z ) -> y e. x ) ) )
3 2 aecoms 
 |-  ( A. y y = x -> ( -. x = y -> E. x A. y ( A. x ( E. z x e. y -> A. y x e. z ) -> y e. x ) ) )
4 2 a1d 
 |-  ( A. x x = y -> ( 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 ) ) ) )
5 nfnae 
 |-  F/ y -. A. x x = y
6 nfae 
 |-  F/ y A. y y = z
7 5 6 nfan 
 |-  F/ y ( -. A. x x = y /\ A. y y = z )
8 el 
 |-  E. w x e. w
9 nfcvf2 
 |-  ( -. A. x x = y -> F/_ y x )
10 nfcvd 
 |-  ( -. A. x x = y -> F/_ y w )
11 9 10 nfeld 
 |-  ( -. A. x x = y -> F/ y x e. w )
12 elequ2 
 |-  ( w = y -> ( x e. w <-> x e. y ) )
13 12 a1i 
 |-  ( -. A. x x = y -> ( w = y -> ( x e. w <-> x e. y ) ) )
14 5 11 13 cbvexd 
 |-  ( -. A. x x = y -> ( E. w x e. w <-> E. y x e. y ) )
15 8 14 mpbii 
 |-  ( -. A. x x = y -> E. y x e. y )
16 15 19.8ad 
 |-  ( -. A. x x = y -> E. x E. y x e. y )
17 df-ex 
 |-  ( E. x E. y x e. y <-> -. A. x -. E. y x e. y )
18 16 17 sylib 
 |-  ( -. A. x x = y -> -. A. x -. E. y x e. y )
19 18 adantr 
 |-  ( ( -. A. x x = y /\ A. y y = z ) -> -. A. x -. E. y x e. y )
20 biidd 
 |-  ( A. y y = z -> ( -. x e. y <-> -. x e. y ) )
21 20 dral1 
 |-  ( A. y y = z -> ( A. y -. x e. y <-> A. z -. x e. y ) )
22 alnex 
 |-  ( A. y -. x e. y <-> -. E. y x e. y )
23 alnex 
 |-  ( A. z -. x e. y <-> -. E. z x e. y )
24 21 22 23 3bitr3g 
 |-  ( A. y y = z -> ( -. E. y x e. y <-> -. E. z x e. y ) )
25 nd2 
 |-  ( A. y y = z -> -. A. y x e. z )
26 mtt 
 |-  ( -. A. y x e. z -> ( -. E. z x e. y <-> ( E. z x e. y -> A. y x e. z ) ) )
27 25 26 syl 
 |-  ( A. y y = z -> ( -. E. z x e. y <-> ( E. z x e. y -> A. y x e. z ) ) )
28 24 27 bitrd 
 |-  ( A. y y = z -> ( -. E. y x e. y <-> ( E. z x e. y -> A. y x e. z ) ) )
29 28 dral2 
 |-  ( A. y y = z -> ( A. x -. E. y x e. y <-> A. x ( E. z x e. y -> A. y x e. z ) ) )
30 29 adantl 
 |-  ( ( -. A. x x = y /\ A. y y = z ) -> ( A. x -. E. y x e. y <-> A. x ( E. z x e. y -> A. y x e. z ) ) )
31 19 30 mtbid 
 |-  ( ( -. A. x x = y /\ A. y y = z ) -> -. A. x ( E. z x e. y -> A. y x e. z ) )
32 31 pm2.21d 
 |-  ( ( -. A. x x = y /\ A. y y = z ) -> ( A. x ( E. z x e. y -> A. y x e. z ) -> y e. x ) )
33 7 32 alrimi 
 |-  ( ( -. A. x x = y /\ A. y y = z ) -> A. y ( A. x ( E. z x e. y -> A. y x e. z ) -> y e. x ) )
34 33 19.8ad 
 |-  ( ( -. A. x x = y /\ A. y y = z ) -> E. x A. y ( A. x ( E. z x e. y -> A. y x e. z ) -> y e. x ) )
35 34 a1d 
 |-  ( ( -. A. x x = y /\ 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 ) ) )
36 35 ex 
 |-  ( -. A. x x = y -> ( 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 ) ) ) )
37 4 36 pm2.61i 
 |-  ( 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 ) ) )
38 1 3 37 pm2.61ii 
 |-  ( -. x = y -> E. x A. y ( A. x ( E. z x e. y -> A. y x e. z ) -> y e. x ) )