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

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 C\right)\to \left(A=B\vee A=C\right)$$
3		neneq	$$⊢A\ne C\to \neg A=C$$
4	3	adantl	$$⊢\left(A\in \left\{B,C\right\}\wedge A\ne C\right)\to \neg A=C$$
5	2 4	olcnd	$$⊢\left(A\in \left\{B,C\right\}\wedge A\ne C\right)\to A=B$$