Theorem neldifpr2

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

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

Proof

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