Metamath Proof Explorer

Theorem elpwid

Description: An element of a power class is a subclass. Deduction form of elpwi . (Contributed by David Moews, 1-May-2017)

Ref Expression
Hypothesis elpwid.1 
|- ( ph -> A e. ~P B )
Assertion elpwid 
|- ( ph -> A C_ B )

Proof

Step Hyp Ref Expression
1 elpwid.1 
 |-  ( ph -> A e. ~P B )
2 elpwi 
 |-  ( A e. ~P B -> A C_ B )
3 1 2 syl 
 |-  ( ph -> A C_ B )