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 =/= B
	prneli.2	|- A =/= C
Assertion	prneli	|- A e/ { B , C }

Proof

Step	Hyp	Ref	Expression
1		prneli.1	|- A =/= B
2		prneli.2	|- A =/= C
3	1 2	nelpri	|- -. A e. { B , C }
4	3	nelir	|- A e/ { B , C }