This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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$

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$