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\ne B$$
	prneli.2	$$⊢A\ne C$$
Assertion	prneli	$$⊢A\notin \left\{B,C\right\}$$

Proof

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