Metamath Proof Explorer


Theorem elpwi2

Description: Membership in a power class. (Contributed by Glauco Siliprandi, 3-Mar-2021)

Ref Expression
Hypotheses elpwi2.1 B V
elpwi2.2 A B
Assertion elpwi2 A 𝒫 B

Proof

Step Hyp Ref Expression
1 elpwi2.1 B V
2 elpwi2.2 A B
3 elpw2g B V A 𝒫 B A B
4 1 3 ax-mp A 𝒫 B A B
5 2 4 mpbir A 𝒫 B