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	$$⊢\phi \to A\ne B$$
	nelprd.2	$$⊢\phi \to A\ne C$$
Assertion	nelprd	$$⊢\phi \to \neg A\in \left\{B,C\right\}$$

Proof

Step	Hyp	Ref	Expression
1		nelprd.1	$$⊢\phi \to A\ne B$$
2		nelprd.2	$$⊢\phi \to 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	syl2anc	$$⊢\phi \to \neg A\in \left\{B,C\right\}$$