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 
|- ( A = B <-> ~P A = ~P B )

Proof

Step Hyp Ref Expression
1 sspwb 
 |-  ( A C_ B <-> ~P A C_ ~P B )
2 sspwb 
 |-  ( B C_ A <-> ~P B C_ ~P A )
3 1 2 anbi12i 
 |-  ( ( A C_ B /\ B C_ A ) <-> ( ~P A C_ ~P B /\ ~P B C_ ~P A ) )
4 eqss 
 |-  ( A = B <-> ( A C_ B /\ B C_ A ) )
5 eqss 
 |-  ( ~P A = ~P B <-> ( ~P A C_ ~P B /\ ~P B C_ ~P A ) )
6 3 4 5 3bitr4i 
 |-  ( A = B <-> ~P A = ~P B )