Theorem pweq

Description: Equality theorem for power class. (Contributed by NM, 21-Jun-1993) (Proof shortened by BJ, 13-Apr-2024)

	Ref	Expression
Assertion	pweq	$$⊢A=B\to 𝒫A=𝒫B$$

Proof

Step	Hyp	Ref	Expression
1		eqimss	$$⊢A=B\to A\subseteq B$$
2	1	sspwd	$$⊢A=B\to 𝒫A\subseteq 𝒫B$$
3		eqimss2	$$⊢A=B\to B\subseteq A$$
4	3	sspwd	$$⊢A=B\to 𝒫B\subseteq 𝒫A$$
5	2 4	eqssd	$$⊢A=B\to 𝒫A=𝒫B$$