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	⊢ 𝐴 ≠ 𝐵
	prneli.2	⊢ 𝐴 ≠ 𝐶
Assertion	prneli	⊢ 𝐴 ∉ { 𝐵 , 𝐶 }

Proof

Step	Hyp	Ref	Expression
1		prneli.1	⊢ 𝐴 ≠ 𝐵
2		prneli.2	⊢ 𝐴 ≠ 𝐶
3	1 2	nelpri	⊢ ¬ 𝐴 ∈ { 𝐵 , 𝐶 }
4	3	nelir	⊢ 𝐴 ∉ { 𝐵 , 𝐶 }