Theorem elpreq

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

	Ref	Expression
Hypotheses	elpreq.1	⊢ ( 𝜑 → 𝑋 ∈ { 𝐴 , 𝐵 } )
	elpreq.2	⊢ ( 𝜑 → 𝑌 ∈ { 𝐴 , 𝐵 } )
	elpreq.3	⊢ ( 𝜑 → ( 𝑋 = 𝐴 ↔ 𝑌 = 𝐴 ) )
Assertion	elpreq	⊢ ( 𝜑 → 𝑋 = 𝑌 )

Proof

Step	Hyp	Ref	Expression
1		elpreq.1	⊢ ( 𝜑 → 𝑋 ∈ { 𝐴 , 𝐵 } )
2		elpreq.2	⊢ ( 𝜑 → 𝑌 ∈ { 𝐴 , 𝐵 } )
3		elpreq.3	⊢ ( 𝜑 → ( 𝑋 = 𝐴 ↔ 𝑌 = 𝐴 ) )
4		simpr	⊢ ( ( 𝜑 ∧ 𝑋 = 𝐴 ) → 𝑋 = 𝐴 )
5	3	biimpa	⊢ ( ( 𝜑 ∧ 𝑋 = 𝐴 ) → 𝑌 = 𝐴 )
6	4 5	eqtr4d	⊢ ( ( 𝜑 ∧ 𝑋 = 𝐴 ) → 𝑋 = 𝑌 )
7		elpri	⊢ ( 𝑋 ∈ { 𝐴 , 𝐵 } → ( 𝑋 = 𝐴 ∨ 𝑋 = 𝐵 ) )
8	1 7	syl	⊢ ( 𝜑 → ( 𝑋 = 𝐴 ∨ 𝑋 = 𝐵 ) )
9	8	orcanai	⊢ ( ( 𝜑 ∧ ¬ 𝑋 = 𝐴 ) → 𝑋 = 𝐵 )
10		simpl	⊢ ( ( 𝜑 ∧ ¬ 𝑋 = 𝐴 ) → 𝜑 )
11	3	notbid	⊢ ( 𝜑 → ( ¬ 𝑋 = 𝐴 ↔ ¬ 𝑌 = 𝐴 ) )
12	11	biimpa	⊢ ( ( 𝜑 ∧ ¬ 𝑋 = 𝐴 ) → ¬ 𝑌 = 𝐴 )
13		elpri	⊢ ( 𝑌 ∈ { 𝐴 , 𝐵 } → ( 𝑌 = 𝐴 ∨ 𝑌 = 𝐵 ) )
14		pm2.53	⊢ ( ( 𝑌 = 𝐴 ∨ 𝑌 = 𝐵 ) → ( ¬ 𝑌 = 𝐴 → 𝑌 = 𝐵 ) )
15	2 13 14	3syl	⊢ ( 𝜑 → ( ¬ 𝑌 = 𝐴 → 𝑌 = 𝐵 ) )
16	10 12 15	sylc	⊢ ( ( 𝜑 ∧ ¬ 𝑋 = 𝐴 ) → 𝑌 = 𝐵 )
17	9 16	eqtr4d	⊢ ( ( 𝜑 ∧ ¬ 𝑋 = 𝐴 ) → 𝑋 = 𝑌 )
18	6 17	pm2.61dan	⊢ ( 𝜑 → 𝑋 = 𝑌 )