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

Metamath Proof Explorer

Theorem axpweq

Description: Two equivalent ways to express the Power Set Axiom. Note that ax-pow is not used by the proof. When ax-pow is assumed and A is a set, both sides of the biconditional hold. In ZF, both sides hold if and only if A is a set (see pwexr ). (Contributed by NM, 22-Jun-2009)

Ref Expression
Assertion axpweq 
|- ( ~P A e. _V <-> E. x A. y ( A. z ( z e. y -> z e. A ) -> y e. x ) )

Proof

Step Hyp Ref Expression
1 pwidg 
 |-  ( ~P A e. _V -> ~P A e. ~P ~P A )
2 pweq 
 |-  ( x = ~P A -> ~P x = ~P ~P A )
3 2 eleq2d 
 |-  ( x = ~P A -> ( ~P A e. ~P x <-> ~P A e. ~P ~P A ) )
4 3 spcegv 
 |-  ( ~P A e. _V -> ( ~P A e. ~P ~P A -> E. x ~P A e. ~P x ) )
5 1 4 mpd 
 |-  ( ~P A e. _V -> E. x ~P A e. ~P x )
6 elex 
 |-  ( ~P A e. ~P x -> ~P A e. _V )
7 6 exlimiv 
 |-  ( E. x ~P A e. ~P x -> ~P A e. _V )
8 5 7 impbii 
 |-  ( ~P A e. _V <-> E. x ~P A e. ~P x )
9 vex 
 |-  x e. _V
10 9 elpw2 
 |-  ( ~P A e. ~P x <-> ~P A C_ x )
11 pwss 
 |-  ( ~P A C_ x <-> A. y ( y C_ A -> y e. x ) )
12 df-ss 
 |-  ( y C_ A <-> A. z ( z e. y -> z e. A ) )
13 12 imbi1i 
 |-  ( ( y C_ A -> y e. x ) <-> ( A. z ( z e. y -> z e. A ) -> y e. x ) )
14 13 albii 
 |-  ( A. y ( y C_ A -> y e. x ) <-> A. y ( A. z ( z e. y -> z e. A ) -> y e. x ) )
15 11 14 bitri 
 |-  ( ~P A C_ x <-> A. y ( A. z ( z e. y -> z e. A ) -> y e. x ) )
16 10 15 bitri 
 |-  ( ~P A e. ~P x <-> A. y ( A. z ( z e. y -> z e. A ) -> y e. x ) )
17 16 exbii 
 |-  ( E. x ~P A e. ~P x <-> E. x A. y ( A. z ( z e. y -> z e. A ) -> y e. x ) )
18 8 17 bitri 
 |-  ( ~P A e. _V <-> E. x A. y ( A. z ( z e. y -> z e. A ) -> y e. x ) )