Theorem elpreq

Description: Equality wihin a pair. (Contributed by Thierry Arnoux, 23-Aug-2017)

	Ref	Expression
Hypotheses	elpreq.1	$$⊢\phi \to X\in \left\{A,B\right\}$$
	elpreq.2	$$⊢\phi \to Y\in \left\{A,B\right\}$$
	elpreq.3	$$⊢\phi \to \left(X=A\leftrightarrow Y=A\right)$$
Assertion	elpreq	$$⊢\phi \to X=Y$$

Proof

Step	Hyp	Ref	Expression
1		elpreq.1	$$⊢\phi \to X\in \left\{A,B\right\}$$
2		elpreq.2	$$⊢\phi \to Y\in \left\{A,B\right\}$$
3		elpreq.3	$$⊢\phi \to \left(X=A\leftrightarrow Y=A\right)$$
4		simpr	$$⊢\left(\phi \wedge X=A\right)\to X=A$$
5	3	biimpa	$$⊢\left(\phi \wedge X=A\right)\to Y=A$$
6	4 5	eqtr4d	$$⊢\left(\phi \wedge X=A\right)\to X=Y$$
7		elpri	$$⊢X\in \left\{A,B\right\}\to \left(X=A\vee X=B\right)$$
8	1 7	syl	$$⊢\phi \to \left(X=A\vee X=B\right)$$
9	8	orcanai	$$⊢\left(\phi \wedge \neg X=A\right)\to X=B$$
10		simpl	$$⊢\left(\phi \wedge \neg X=A\right)\to \phi$$
11	3	notbid	$$⊢\phi \to \left(\neg X=A\leftrightarrow \neg Y=A\right)$$
12	11	biimpa	$$⊢\left(\phi \wedge \neg X=A\right)\to \neg Y=A$$
13		elpri	$$⊢Y\in \left\{A,B\right\}\to \left(Y=A\vee Y=B\right)$$
14		pm2.53	$$⊢\left(Y=A\vee Y=B\right)\to \left(\neg Y=A\to Y=B\right)$$
15	2 13 14	3syl	$$⊢\phi \to \left(\neg Y=A\to Y=B\right)$$
16	10 12 15	sylc	$$⊢\left(\phi \wedge \neg X=A\right)\to Y=B$$
17	9 16	eqtr4d	$$⊢\left(\phi \wedge \neg X=A\right)\to X=Y$$
18	6 17	pm2.61dan	$$⊢\phi \to X=Y$$