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 φ A 𝒫 B
Assertion elpwid φ A B


Step Hyp Ref Expression
1 elpwid.1 φ A 𝒫 B
2 elpwi A 𝒫 B A B
3 1 2 syl φ A B