Description: Subset relation implied by membership in a power class. (Contributed by NM, 17Feb2007)
Ref  Expression  

Assertion  elpwi   ( A e. ~P B > A C_ B ) 
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 ) 