This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.
Database ZF (ZERMELO-FRAENKEL) SET THEORY ZF Set Theory - start with the Axiom of Extensionality Power classes 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 ⊢ ( 𝐴 = 𝐵 → 𝒫 𝐴 = 𝒫 𝐵 )