Theorem nelne1

Description: Two classes are different if they don't contain the same element. (Contributed by NM, 3-Feb-2012) (Proof shortened by Wolf Lammen, 14-May-2023)

	Ref	Expression
Assertion	nelne1	$$⊢\left(A\in B\wedge \neg A\in C\right)\to B\ne C$$

Proof

Step	Hyp	Ref	Expression
1		nelneq2	$$⊢\left(A\in B\wedge \neg A\in C\right)\to \neg B=C$$
2	1	neqned	$$⊢\left(A\in B\wedge \neg A\in C\right)\to B\ne C$$