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		neneq	|- ( A =/= C -> -. A = C )
2	1	adantl	|- ( ( A e. { B , C } /\ A =/= C ) -> -. A = C )
3		elpri	|- ( A e. { B , C } -> ( A = B \/ A = C ) )
4	3	adantr	|- ( ( A e. { B , C } /\ A =/= C ) -> ( A = B \/ A = C ) )
5		orcom	|- ( ( A = B \/ A = C ) <-> ( A = C \/ A = B ) )
6		df-or	|- ( ( A = C \/ A = B ) <-> ( -. A = C -> A = B ) )
7	5 6	bitri	|- ( ( A = B \/ A = C ) <-> ( -. A = C -> A = B ) )
8	4 7	sylib	|- ( ( A e. { B , C } /\ A =/= C ) -> ( -. A = C -> A = B ) )
9	2 8	mpd	|- ( ( A e. { B , C } /\ A =/= C ) -> A = B )