Theorem neldifpr1

Description: The first element of a pair is not an element of a difference with this pair. (Contributed by Thierry Arnoux, 20-Nov-2023)

	Ref	Expression
Assertion	neldifpr1	⊢ ¬ 𝐴 ∈ ( 𝐶 ∖ { 𝐴 , 𝐵 } )

Proof

Step	Hyp	Ref	Expression
1		neirr	⊢ ¬ 𝐴 ≠ 𝐴
2		eldifpr	⊢ ( 𝐴 ∈ ( 𝐶 ∖ { 𝐴 , 𝐵 } ) ↔ ( 𝐴 ∈ 𝐶 ∧ 𝐴 ≠ 𝐴 ∧ 𝐴 ≠ 𝐵 ) )
3	2	simp2bi	⊢ ( 𝐴 ∈ ( 𝐶 ∖ { 𝐴 , 𝐵 } ) → 𝐴 ≠ 𝐴 )
4	1 3	mto	⊢ ¬ 𝐴 ∈ ( 𝐶 ∖ { 𝐴 , 𝐵 } )