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

Metamath Proof Explorer

Theorem pweqALT

Description: Alternate proof of pweq directly from the definition. (Contributed by NM, 21-Jun-1993) (Proof modification is discouraged.) (New usage is discouraged.)

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

Proof

Step	Hyp	Ref	Expression
1		sseq2	$⊢ A = B \to (x \subseteq A \leftrightarrow x \subseteq B)$
2	1	abbidv	$⊢ A = B \to \{x \| x \subseteq A\} = \{x \| x \subseteq B\}$
3		df-pw	$⊢ 𝒫 A = \{x \| x \subseteq A\}$
4		df-pw	$⊢ 𝒫 B = \{x \| x \subseteq B\}$
5	2 3 4	3eqtr4g	$⊢ A = B \to 𝒫 A = 𝒫 B$