Theorem elprn2

Description: A member of an unordered pair that is not the "second", must be the "first". (Contributed by Glauco Siliprandi, 11-Dec-2019)

	Ref	Expression
Assertion	elprn2	|- ( ( A e. { B , C } /\ A =/= C ) -> A = B )

Proof

Step	Hyp	Ref	Expression
1		elpri	|- ( A e. { B , C } -> ( A = B \/ A = C ) )
2	1	adantr	|- ( ( A e. { B , C } /\ A =/= C ) -> ( A = B \/ A = C ) )
3		neneq	|- ( A =/= C -> -. A = C )
4	3	adantl	|- ( ( A e. { B , C } /\ A =/= C ) -> -. A = C )
5	2 4	olcnd	|- ( ( A e. { B , C } /\ A =/= C ) -> A = B )