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