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	$$⊢A=B\leftrightarrow 𝒫A=𝒫B$$

Proof

Step	Hyp	Ref	Expression
1		sspwb	$$⊢A\subseteq B\leftrightarrow 𝒫A\subseteq 𝒫B$$
2		sspwb	$$⊢B\subseteq A\leftrightarrow 𝒫B\subseteq 𝒫A$$
3	1 2	anbi12i	$$⊢\left(A\subseteq B\wedge B\subseteq A\right)\leftrightarrow \left(𝒫A\subseteq 𝒫B\wedge 𝒫B\subseteq 𝒫A\right)$$
4		eqss	$$⊢A=B\leftrightarrow \left(A\subseteq B\wedge B\subseteq A\right)$$
5		eqss	$$⊢𝒫A=𝒫B\leftrightarrow \left(𝒫A\subseteq 𝒫B\wedge 𝒫B\subseteq 𝒫A\right)$$
6	3 4 5	3bitr4i	$$⊢A=B\leftrightarrow 𝒫A=𝒫B$$