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