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\subseteq B\to \neg B\subset A$$

Proof

Step	Hyp	Ref	Expression
1		dfpss3	$$⊢B\subset A\leftrightarrow \left(B\subseteq A\wedge \neg A\subseteq B\right)$$
2	1	simprbi	$$⊢B\subset A\to \neg A\subseteq B$$
3	2	con2i	$$⊢A\subseteq B\to \neg B\subset A$$