This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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

Step	Hyp	Ref	Expression
1		neirr	$⊢ \neg B \neq B$
2		eldifpr	$⊢ B \in (C ∖ \{A, B\}) \leftrightarrow (B \in C \land B \neq A \land B \neq B)$
3	2	simp3bi	$⊢ B \in (C ∖ \{A, B\}) \to B \neq B$
4	1 3	mto	$⊢ \neg B \in (C ∖ \{A, B\})$