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

Metamath Proof Explorer

Theorem pweqb

Description: Classes are equal if and only if their power classes are equal. Exercise 19 of TakeutiZaring p. 18. (Contributed by NM, 13-Oct-1996)

Ref Expression
Assertion pweqb ( 𝐴 = 𝐵 ↔ 𝒫 𝐴 = 𝒫 𝐵 )

Proof

Step Hyp Ref Expression
1 sspwb ⊢ ( 𝐴 ⊆ 𝐵 ↔ 𝒫 𝐴 ⊆ 𝒫 𝐵 )
2 sspwb ⊢ ( 𝐵 ⊆ 𝐴 ↔ 𝒫 𝐵 ⊆ 𝒫 𝐴 )
3 1 2 anbi12i ⊢ ( ( 𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝐴 ) ↔ ( 𝒫 𝐴 ⊆ 𝒫 𝐵 ∧ 𝒫 𝐵 ⊆ 𝒫 𝐴 ) )
4 eqss ⊢ ( 𝐴 = 𝐵 ↔ ( 𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝐴 ) )
5 eqss ⊢ ( 𝒫 𝐴 = 𝒫 𝐵 ↔ ( 𝒫 𝐴 ⊆ 𝒫 𝐵 ∧ 𝒫 𝐵 ⊆ 𝒫 𝐴 ) )
6 3 4 5 3bitr4i ⊢ ( 𝐴 = 𝐵 ↔ 𝒫 𝐴 = 𝒫 𝐵 )