Metamath Proof Explorer


Theorem pweqi

Description: Equality inference for power class. (Contributed by NM, 27-Nov-2013)

Ref Expression
Hypothesis pweqi.1 A=B
Assertion pweqi 𝒫A=𝒫B

Proof

Step Hyp Ref Expression
1 pweqi.1 A=B
2 pweq A=B𝒫A=𝒫B
3 1 2 ax-mp 𝒫A=𝒫B