Theorem nelelne

Description: Two classes are different if they don't belong to the same class. (Contributed by Rodolfo Medina, 17-Oct-2010) (Proof shortened by AV, 10-May-2020)

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

Proof

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