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	$$⊢\neg B\in \left(C\setminus \left\{A,B\right\}\right)$$

Proof

Step	Hyp	Ref	Expression
1		neirr	$$⊢\neg B\ne B$$
2		eldifpr	$$⊢B\in \left(C\setminus \left\{A,B\right\}\right)\leftrightarrow \left(B\in C\wedge B\ne A\wedge B\ne B\right)$$
3	2	simp3bi	$$⊢B\in \left(C\setminus \left\{A,B\right\}\right)\to B\ne B$$
4	1 3	mto	$$⊢\neg B\in \left(C\setminus \left\{A,B\right\}\right)$$