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

Metamath Proof Explorer

Theorem nelne2

Description: Two classes are different if they don't belong to the same class. (Contributed by NM, 25-Jun-2012) (Proof shortened by Wolf Lammen, 14-May-2023)

		Ref	Expression
	Assertion	nelne2	$⊢ (A \in C \land \neg B \in C) \to A \neq B$

Proof

Step	Hyp	Ref	Expression
1		nelneq	$⊢ (A \in C \land \neg B \in C) \to \neg A = B$
2	1	neqned	$⊢ (A \in C \land \neg B \in C) \to A \neq B$