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	$$⊢\left(A\in \left\{B,C\right\}\wedge A\ne B\right)\to A=C$$

Proof

Step	Hyp	Ref	Expression
1		elpri	$$⊢A\in \left\{B,C\right\}\to \left(A=B\vee A=C\right)$$
2	1	adantr	$$⊢\left(A\in \left\{B,C\right\}\wedge A\ne B\right)\to \left(A=B\vee A=C\right)$$
3		neneq	$$⊢A\ne B\to \neg A=B$$
4	3	adantl	$$⊢\left(A\in \left\{B,C\right\}\wedge A\ne B\right)\to \neg A=B$$
5	2 4	orcnd	$$⊢\left(A\in \left\{B,C\right\}\wedge A\ne B\right)\to A=C$$