Metamath Proof Explorer

Theorem elpw2g

Description: Membership in a power class. Theorem 86 of Suppes p. 47. (Contributed by NM, 7-Aug-2000)

Ref Expression
Assertion elpw2g 
|- ( B e. V -> ( A e. ~P B <-> A C_ B ) )

Proof

Step Hyp Ref Expression
1 elpwi 
 |-  ( A e. ~P B -> A C_ B )
2 ssexg 
 |-  ( ( A C_ B /\ B e. V ) -> A e. _V )
3 elpwg 
 |-  ( A e. _V -> ( A e. ~P B <-> A C_ B ) )
4 3 biimparc 
 |-  ( ( A C_ B /\ A e. _V ) -> A e. ~P B )
5 2 4 syldan 
 |-  ( ( A C_ B /\ B e. V ) -> A e. ~P B )
6 5 expcom 
 |-  ( B e. V -> ( A C_ B -> A e. ~P B ) )
7 1 6 impbid2 
 |-  ( B e. V -> ( A e. ~P B <-> A C_ B ) )