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

Metamath Proof Explorer

Theorem elpw2

Description: Membership in a power class. Theorem 86 of Suppes p. 47. (Contributed by NM, 11-Oct-2007)

Ref Expression
Hypothesis elpw2.1 
|- B e. _V
Assertion elpw2 
|- ( A e. ~P B <-> A C_ B )

Proof

Step Hyp Ref Expression
1 elpw2.1 
 |-  B e. _V
2 elpw2g 
 |-  ( B e. _V -> ( A e. ~P B <-> A C_ B ) )
3 1 2 ax-mp 
 |-  ( A e. ~P B <-> A C_ B )