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

Metamath Proof Explorer

Theorem eqelbid

Description: A variable elimination law for equality within a given set A . See equvel . (Contributed by Thierry Arnoux, 20-Feb-2025)

Ref Expression
Hypotheses eqelbid.1 ⊢ φ → B ∈ A
eqelbid.2 ⊢ φ → C ∈ A
Assertion eqelbid ⊢ φ → ∀ x ∈ A x = B ↔ x = C ↔ B = C

Proof

Step Hyp Ref Expression
1 eqelbid.1 ⊢ φ → B ∈ A
2 eqelbid.2 ⊢ φ → C ∈ A
3 eqeq1 ⊢ x = B → x = B ↔ B = B
4 eqeq1 ⊢ x = B → x = C ↔ B = C
5 3 4 bibi12d ⊢ x = B → x = B ↔ x = C ↔ B = B ↔ B = C
6 eqid ⊢ B = B
7 6 tbt ⊢ B = C ↔ B = C ↔ B = B
8 bicom ⊢ B = C ↔ B = B ↔ B = B ↔ B = C
9 7 8 bitri ⊢ B = C ↔ B = B ↔ B = C
10 5 9 bitr4di ⊢ x = B → x = B ↔ x = C ↔ B = C
11 simpr ⊢ φ ∧ ∀ x ∈ A x = B ↔ x = C → ∀ x ∈ A x = B ↔ x = C
12 1 adantr ⊢ φ ∧ ∀ x ∈ A x = B ↔ x = C → B ∈ A
13 10 11 12 rspcdva ⊢ φ ∧ ∀ x ∈ A x = B ↔ x = C → B = C
14 simplr ⊢ φ ∧ B = C ∧ x ∈ A → B = C
15 14 eqeq2d ⊢ φ ∧ B = C ∧ x ∈ A → x = B ↔ x = C
16 15 ralrimiva ⊢ φ ∧ B = C → ∀ x ∈ A x = B ↔ x = C
17 13 16 impbida ⊢ φ → ∀ x ∈ A x = B ↔ x = C ↔ B = C