Theorem nelss

Description: Demonstrate by witnesses that two classes lack a subclass relation. (Contributed by Stefan O'Rear, 5-Feb-2015)

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

Proof

Step	Hyp	Ref	Expression
1		ssel	$$⊢B\subseteq C\to \left(A\in B\to A\in C\right)$$
2	1	com12	$$⊢A\in B\to \left(B\subseteq C\to A\in C\right)$$
3	2	con3dimp	$$⊢\left(A\in B\wedge \neg A\in C\right)\to \neg B\subseteq C$$