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

Metamath Proof Explorer

Theorem elnelne1

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

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

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