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

Metamath Proof Explorer

Theorem elnelne2

Description: Two classes are different if they don't belong to the same class. (Contributed by AV, 28-Jan-2020)

		Ref	Expression
	Assertion	elnelne2	$⊢ (A \in C \land B \notin C) \to A \neq B$

Step	Hyp	Ref	Expression
1		df-nel	$⊢ B \notin C \leftrightarrow \neg B \in C$
2		nelne2	$⊢ (A \in C \land \neg B \in C) \to A \neq B$
3	1 2	sylan2b	$⊢ (A \in C \land B \notin C) \to A \neq B$