Theorem elndif

Description: A set does not belong to a class excluding it. (Contributed by NM, 27-Jun-1994)

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

Proof

Step	Hyp	Ref	Expression
1		eldifn	$$⊢A\in \left(C\setminus B\right)\to \neg A\in B$$
2	1	con2i	$$⊢A\in B\to \neg A\in \left(C\setminus B\right)$$