Theorem eldifsnneq

Description: An element of a difference with a singleton is not equal to the element of that singleton. Note that ( -. A e. { C } -> -. A = C ) need not hold if A is a proper class. (Contributed by BJ, 18-Mar-2023) (Proof shortened by Steven Nguyen, 1-Jun-2023)

	Ref	Expression
Assertion	eldifsnneq	$$⊢A\in \left(B\setminus \left\{C\right\}\right)\to \neg A=C$$

Proof

Step	Hyp	Ref	Expression
1		eldifsni	$$⊢A\in \left(B\setminus \left\{C\right\}\right)\to A\ne C$$
2	1	neneqd	$$⊢A\in \left(B\setminus \left\{C\right\}\right)\to \neg A=C$$