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 \left(x\subseteq A\leftrightarrow x\subseteq B\right)$$
2	1	abbidv	$$⊢A=B\to \left\{x|x\subseteq A\right\}=\left\{x|x\subseteq B\right\}$$
3		df-pw	$$⊢𝒫A=\left\{x|x\subseteq A\right\}$$
4		df-pw	$$⊢𝒫B=\left\{x|x\subseteq B\right\}$$
5	2 3 4	3eqtr4g	$$⊢A=B\to 𝒫A=𝒫B$$