Metamath Proof Explorer


Theorem elpwi2

Description: Membership in a power class. (Contributed by Glauco Siliprandi, 3-Mar-2021) (Proof shortened by Wolf Lammen, 26-May-2024)

Ref Expression
Hypotheses elpwi2.1 BV
elpwi2.2 AB
Assertion elpwi2 A𝒫B

Proof

Step Hyp Ref Expression
1 elpwi2.1 BV
2 elpwi2.2 AB
3 1 elexi BV
4 3 elpw2 A𝒫BAB
5 2 4 mpbir A𝒫B