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

Metamath Proof Explorer

Theorem prneli

Description: If an element doesn't match the items in an unordered pair, it is not in the unordered pair, using e/ . (Contributed by David A. Wheeler, 10-May-2015)

	Ref	Expression
Hypotheses	prneli.1	$⊢ A \neq B$
	prneli.2	$⊢ A \neq C$
Assertion	prneli	$⊢ A \notin \{B, C\}$

Proof

Step	Hyp	Ref	Expression
1		prneli.1	$⊢ A \neq B$
2		prneli.2	$⊢ A \neq C$
3	1 2	nelpri	$⊢ \neg A \in \{B, C\}$
4	3	nelir	$⊢ A \notin \{B, C\}$