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