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 e. ( B \ { C } ) -> -. A = C )

Proof

Step	Hyp	Ref	Expression
1		eldifsni	|- ( A e. ( B \ { C } ) -> A =/= C )
2	1	neneqd	|- ( A e. ( B \ { C } ) -> -. A = C )