This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem nssne2

Description: Two classes are different if they are not subclasses of the same class. (Contributed by NM, 23-Apr-2015)

		Ref	Expression
	Assertion	nssne2	$⊢ (A \subseteq C \land \neg B \subseteq C) \to A \neq B$

Step	Hyp	Ref	Expression
1		sseq1	$⊢ A = B \to (A \subseteq C \leftrightarrow B \subseteq C)$
2	1	biimpcd	$⊢ A \subseteq C \to (A = B \to B \subseteq C)$
3	2	necon3bd	$⊢ A \subseteq C \to (\neg B \subseteq C \to A \neq B)$
4	3	imp	$⊢ (A \subseteq C \land \neg B \subseteq C) \to A \neq B$