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	⊢ ( 𝐴 = 𝐵 → 𝒫 𝐴 = 𝒫 𝐵 )

Proof

Step	Hyp	Ref	Expression
1		sseq2	⊢ ( 𝐴 = 𝐵 → ( 𝑥 ⊆ 𝐴 ↔ 𝑥 ⊆ 𝐵 ) )
2	1	abbidv	⊢ ( 𝐴 = 𝐵 → { 𝑥 ∣ 𝑥 ⊆ 𝐴 } = { 𝑥 ∣ 𝑥 ⊆ 𝐵 } )
3		df-pw	⊢ 𝒫 𝐴 = { 𝑥 ∣ 𝑥 ⊆ 𝐴 }
4		df-pw	⊢ 𝒫 𝐵 = { 𝑥 ∣ 𝑥 ⊆ 𝐵 }
5	2 3 4	3eqtr4g	⊢ ( 𝐴 = 𝐵 → 𝒫 𝐴 = 𝒫 𝐵 )