Description: Classes are proper subclasses if and only if their power classes are proper subclasses. (Contributed by Steven Nguyen, 17-Jul-2022)
Ref | Expression | ||
---|---|---|---|
Assertion | psspwb | |- ( A C. B <-> ~P A C. ~P B ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | sspwb | |- ( A C_ B <-> ~P A C_ ~P B ) |
|
2 | pweqb | |- ( A = B <-> ~P A = ~P B ) |
|
3 | 2 | necon3bii | |- ( A =/= B <-> ~P A =/= ~P B ) |
4 | 1 3 | anbi12i | |- ( ( A C_ B /\ A =/= B ) <-> ( ~P A C_ ~P B /\ ~P A =/= ~P B ) ) |
5 | df-pss | |- ( A C. B <-> ( A C_ B /\ A =/= B ) ) |
|
6 | df-pss | |- ( ~P A C. ~P B <-> ( ~P A C_ ~P B /\ ~P A =/= ~P B ) ) |
|
7 | 4 5 6 | 3bitr4i | |- ( A C. B <-> ~P A C. ~P B ) |