Metamath Proof Explorer


Theorem psspwb

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 )

Proof

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 )