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		neneq	$$⊢A\ne C\to \neg A=C$$
2	1	adantl	$$⊢\left(A\in \left\{B,C\right\}\wedge A\ne C\right)\to \neg A=C$$
3		elpri	$$⊢A\in \left\{B,C\right\}\to \left(A=B\vee A=C\right)$$
4	3	adantr	$$⊢\left(A\in \left\{B,C\right\}\wedge A\ne C\right)\to \left(A=B\vee A=C\right)$$
5		orcom	$$⊢\left(A=B\vee A=C\right)\leftrightarrow \left(A=C\vee A=B\right)$$
6		df-or	$$⊢\left(A=C\vee A=B\right)\leftrightarrow \left(\neg A=C\to A=B\right)$$
7	5 6	bitri	$$⊢\left(A=B\vee A=C\right)\leftrightarrow \left(\neg A=C\to A=B\right)$$
8	4 7	sylib	$$⊢\left(A\in \left\{B,C\right\}\wedge A\ne C\right)\to \left(\neg A=C\to A=B\right)$$
9	2 8	mpd	$$⊢\left(A\in \left\{B,C\right\}\wedge A\ne C\right)\to A=B$$