This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ⊢ ( 𝜑 → 𝑋 = 𝑌 )