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 ) |
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 ) |