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\to 𝒫A=𝒫B$$
3	1 2	ax-mp	$$⊢𝒫A=𝒫B$$