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

Proof

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