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