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

Metamath Proof Explorer

Theorem nelprd

Description: If an element doesn't match the items in an unordered pair, it is not in the unordered pair, deduction version. (Contributed by Alexander van der Vekens, 25-Jan-2018)

	Ref	Expression
Hypotheses	nelprd.1	$⊢ φ \to A \neq B$
	nelprd.2	$⊢ φ \to A \neq C$
Assertion	nelprd	$⊢ φ \to \neg A \in \{B, C\}$

Proof

Step	Hyp	Ref	Expression
1		nelprd.1	$⊢ φ \to A \neq B$
2		nelprd.2	$⊢ φ \to A \neq C$
3		neanior	$⊢ (A \neq B \land A \neq C) \leftrightarrow \neg (A = B \lor A = C)$
4		elpri	$⊢ A \in \{B, C\} \to (A = B \lor A = C)$
5	4	con3i	$⊢ \neg (A = B \lor A = C) \to \neg A \in \{B, C\}$
6	3 5	sylbi	$⊢ (A \neq B \land A \neq C) \to \neg A \in \{B, C\}$
7	1 2 6	syl2anc	$⊢ φ \to \neg A \in \{B, C\}$