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

Proof

Step	Hyp	Ref	Expression
1		nelpri.1	|- A =/= B
2		nelpri.2	|- A =/= C
3		neanior	|- ( ( A =/= B /\ A =/= C ) <-> -. ( A = B \/ A = C ) )
4		elpri	|- ( A e. { B , C } -> ( A = B \/ A = C ) )
5	4	con3i	|- ( -. ( A = B \/ A = C ) -> -. A e. { B , C } )
6	3 5	sylbi	|- ( ( A =/= B /\ A =/= C ) -> -. A e. { B , C } )
7	1 2 6	mp2an	|- -. A e. { B , C }