Theorem elpreq

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

	Ref	Expression
Hypotheses	elpreq.1	|- ( ph -> X e. { A , B } )
	elpreq.2	|- ( ph -> Y e. { A , B } )
	elpreq.3	|- ( ph -> ( X = A <-> Y = A ) )
Assertion	elpreq	|- ( ph -> X = Y )

Proof

Step	Hyp	Ref	Expression
1		elpreq.1	|- ( ph -> X e. { A , B } )
2		elpreq.2	|- ( ph -> Y e. { A , B } )
3		elpreq.3	|- ( ph -> ( X = A <-> Y = A ) )
4		simpr	|- ( ( ph /\ X = A ) -> X = A )
5	3	biimpa	|- ( ( ph /\ X = A ) -> Y = A )
6	4 5	eqtr4d	|- ( ( ph /\ X = A ) -> X = Y )
7		elpri	|- ( X e. { A , B } -> ( X = A \/ X = B ) )
8	1 7	syl	|- ( ph -> ( X = A \/ X = B ) )
9	8	orcanai	|- ( ( ph /\ -. X = A ) -> X = B )
10		simpl	|- ( ( ph /\ -. X = A ) -> ph )
11	3	notbid	|- ( ph -> ( -. X = A <-> -. Y = A ) )
12	11	biimpa	|- ( ( ph /\ -. X = A ) -> -. Y = A )
13		elpri	|- ( Y e. { A , B } -> ( Y = A \/ Y = B ) )
14		pm2.53	|- ( ( Y = A \/ Y = B ) -> ( -. Y = A -> Y = B ) )
15	2 13 14	3syl	|- ( ph -> ( -. Y = A -> Y = B ) )
16	10 12 15	sylc	|- ( ( ph /\ -. X = A ) -> Y = B )
17	9 16	eqtr4d	|- ( ( ph /\ -. X = A ) -> X = Y )
18	6 17	pm2.61dan	|- ( ph -> X = Y )