Theorem nssne1

Description: Two classes are different if they don't include the same class. (Contributed by NM, 23-Apr-2015)

	Ref	Expression
Assertion	nssne1	$$⊢\left(A\subseteq B\wedge \neg A\subseteq C\right)\to B\ne C$$

Proof

Step	Hyp	Ref	Expression
1		sseq2	$$⊢B=C\to \left(A\subseteq B\leftrightarrow A\subseteq C\right)$$
2	1	biimpcd	$$⊢A\subseteq B\to \left(B=C\to A\subseteq C\right)$$
3	2	necon3bd	$$⊢A\subseteq B\to \left(\neg A\subseteq C\to B\ne C\right)$$
4	3	imp	$$⊢\left(A\subseteq B\wedge \neg A\subseteq C\right)\to B\ne C$$