Theorem elprn1

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

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

Proof

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