Metamath Proof Explorer

Theorem pssnssi

Description: A proper subclass does not include the other class. (Contributed by Glauco Siliprandi, 26-Jun-2021)

Ref Expression
Hypothesis pssnssi.1 
|- A C. B
Assertion pssnssi 
|- -. B C_ A

Proof

Step Hyp Ref Expression
1 pssnssi.1 
 |-  A C. B
2 dfpss3 
 |-  ( A C. B <-> ( A C_ B /\ -. B C_ A ) )
3 1 2 mpbi 
 |-  ( A C_ B /\ -. B C_ A )
4 3 simpri 
 |-  -. B C_ A