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 ( 𝐴𝐵 → ¬ 𝐵𝐴 )

Proof

Step Hyp Ref Expression
1 dfpss3 ( 𝐵𝐴 ↔ ( 𝐵𝐴 ∧ ¬ 𝐴𝐵 ) )
2 1 simprbi ( 𝐵𝐴 → ¬ 𝐴𝐵 )
3 2 con2i ( 𝐴𝐵 → ¬ 𝐵𝐴 )