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	$$⊢\left(A\in C\wedge B\notin C\right)\to A\ne B$$

Proof

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