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

Proof

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