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 )