Metamath Proof Explorer

Theorem ssnpss

Description: Partial trichotomy law for subclasses. (Contributed by NM, 16-May-1996) (Proof shortened by Andrew Salmon, 26-Jun-2011)

Ref Expression
Assertion ssnpss 
|- ( A C_ B -> -. B C. A )

Proof

Step Hyp Ref Expression
1 dfpss3 
 |-  ( B C. A <-> ( B C_ A /\ -. A C_ B ) )
2 1 simprbi 
 |-  ( B C. A -> -. A C_ B )
3 2 con2i 
 |-  ( A C_ B -> -. B C. A )