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