Theorem nelpri

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

	Ref	Expression
Hypotheses	nelpri.1	$$⊢A\ne B$$
	nelpri.2	$$⊢A\ne C$$
Assertion	nelpri	$$⊢\neg A\in \left\{B,C\right\}$$

Proof

Step	Hyp	Ref	Expression
1		nelpri.1	$$⊢A\ne B$$
2		nelpri.2	$$⊢A\ne C$$
3		neanior	$$⊢\left(A\ne B\wedge A\ne C\right)\leftrightarrow \neg \left(A=B\vee A=C\right)$$
4		elpri	$$⊢A\in \left\{B,C\right\}\to \left(A=B\vee A=C\right)$$
5	4	con3i	$$⊢\neg \left(A=B\vee A=C\right)\to \neg A\in \left\{B,C\right\}$$
6	3 5	sylbi	$$⊢\left(A\ne B\wedge A\ne C\right)\to \neg A\in \left\{B,C\right\}$$
7	1 2 6	mp2an	$$⊢\neg A\in \left\{B,C\right\}$$