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	⊢ ( 𝐴 ∈ ( 𝐵 ∖ { 𝐶 } ) → ¬ 𝐴 = 𝐶 )

Proof

Step	Hyp	Ref	Expression
1		eldifsni	⊢ ( 𝐴 ∈ ( 𝐵 ∖ { 𝐶 } ) → 𝐴 ≠ 𝐶 )
2	1	neneqd	⊢ ( 𝐴 ∈ ( 𝐵 ∖ { 𝐶 } ) → ¬ 𝐴 = 𝐶 )