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		elpri	|- ( A e. { B , C } -> ( A = B \/ A = C ) )
2	1	adantr	|- ( ( A e. { B , C } /\ A =/= B ) -> ( A = B \/ A = C ) )
3		neneq	|- ( A =/= B -> -. A = B )
4	3	adantl	|- ( ( A e. { B , C } /\ A =/= B ) -> -. A = B )
5	2 4	orcnd	|- ( ( A e. { B , C } /\ A =/= B ) -> A = C )