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	|- -. A e. ( C \ { A , B } )

Proof

Step	Hyp	Ref	Expression
1		neirr	|- -. A =/= A
2		eldifpr	|- ( A e. ( C \ { A , B } ) <-> ( A e. C /\ A =/= A /\ A =/= B ) )
3	2	simp2bi	|- ( A e. ( C \ { A , B } ) -> A =/= A )
4	1 3	mto	|- -. A e. ( C \ { A , B } )