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 ⊢ φ → X ∈ A B
elpreq.2 ⊢ φ → Y ∈ A B
elpreq.3 ⊢ φ → X = A ↔ Y = A
Assertion elpreq ⊢ φ → X = Y

Proof

Step Hyp Ref Expression
1 elpreq.1 ⊢ φ → X ∈ A B
2 elpreq.2 ⊢ φ → Y ∈ A B
3 elpreq.3 ⊢ φ → X = A ↔ Y = A
4 simpr ⊢ φ ∧ X = A → X = A
5 3 biimpa ⊢ φ ∧ X = A → Y = A
6 4 5 eqtr4d ⊢ φ ∧ X = A → X = Y
7 elpri ⊢ X ∈ A B → X = A ∨ X = B
8 1 7 syl ⊢ φ → X = A ∨ X = B
9 8 orcanai ⊢ φ ∧ ¬ X = A → X = B
10 simpl ⊢ φ ∧ ¬ X = A → φ
11 3 notbid ⊢ φ → ¬ X = A ↔ ¬ Y = A
12 11 biimpa ⊢ φ ∧ ¬ X = A → ¬ Y = A
13 elpri ⊢ Y ∈ A B → Y = A ∨ Y = B
14 pm2.53 ⊢ Y = A ∨ Y = B → ¬ Y = A → Y = B
15 2 13 14 3syl ⊢ φ → ¬ Y = A → Y = B
16 10 12 15 sylc ⊢ φ ∧ ¬ X = A → Y = B
17 9 16 eqtr4d ⊢ φ ∧ ¬ X = A → X = Y
18 6 17 pm2.61dan ⊢ φ → X = Y