Metamath Proof Explorer

Theorem elpwi

Description: Subset relation implied by membership in a power class. (Contributed by NM, 17-Feb-2007)

Ref Expression
Assertion elpwi 
|- ( A e. ~P B -> A C_ B )

Proof

Step Hyp Ref Expression
1 elpwg 
 |-  ( A e. ~P B -> ( A e. ~P B <-> A C_ B ) )
2 1 ibi 
 |-  ( A e. ~P B -> A C_ B )