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 ⊢ ( 𝜑 → 𝐵 ∈ 𝐴 )
eqelbid.2 ⊢ ( 𝜑 → 𝐶 ∈ 𝐴 )
Assertion eqelbid ( 𝜑 → ( ∀ 𝑥 ∈ 𝐴 ( 𝑥 = 𝐵 ↔ 𝑥 = 𝐶 ) ↔ 𝐵 = 𝐶 ) )

Proof

Step Hyp Ref Expression
1 eqelbid.1 ⊢ ( 𝜑 → 𝐵 ∈ 𝐴 )
2 eqelbid.2 ⊢ ( 𝜑 → 𝐶 ∈ 𝐴 )
3 eqeq1 ⊢ ( 𝑥 = 𝐵 → ( 𝑥 = 𝐵 ↔ 𝐵 = 𝐵 ) )
4 eqeq1 ⊢ ( 𝑥 = 𝐵 → ( 𝑥 = 𝐶 ↔ 𝐵 = 𝐶 ) )
5 3 4 bibi12d ⊢ ( 𝑥 = 𝐵 → ( ( 𝑥 = 𝐵 ↔ 𝑥 = 𝐶 ) ↔ ( 𝐵 = 𝐵 ↔ 𝐵 = 𝐶 ) ) )
6 eqid ⊢ 𝐵 = 𝐵
7 6 tbt ⊢ ( 𝐵 = 𝐶 ↔ ( 𝐵 = 𝐶 ↔ 𝐵 = 𝐵 ) )
8 bicom ⊢ ( ( 𝐵 = 𝐶 ↔ 𝐵 = 𝐵 ) ↔ ( 𝐵 = 𝐵 ↔ 𝐵 = 𝐶 ) )
9 7 8 bitri ⊢ ( 𝐵 = 𝐶 ↔ ( 𝐵 = 𝐵 ↔ 𝐵 = 𝐶 ) )
10 5 9 bitr4di ⊢ ( 𝑥 = 𝐵 → ( ( 𝑥 = 𝐵 ↔ 𝑥 = 𝐶 ) ↔ 𝐵 = 𝐶 ) )
11 simpr ⊢ ( ( 𝜑 ∧ ∀ 𝑥 ∈ 𝐴 ( 𝑥 = 𝐵 ↔ 𝑥 = 𝐶 ) ) → ∀ 𝑥 ∈ 𝐴 ( 𝑥 = 𝐵 ↔ 𝑥 = 𝐶 ) )
12 1 adantr ⊢ ( ( 𝜑 ∧ ∀ 𝑥 ∈ 𝐴 ( 𝑥 = 𝐵 ↔ 𝑥 = 𝐶 ) ) → 𝐵 ∈ 𝐴 )
13 10 11 12 rspcdva ⊢ ( ( 𝜑 ∧ ∀ 𝑥 ∈ 𝐴 ( 𝑥 = 𝐵 ↔ 𝑥 = 𝐶 ) ) → 𝐵 = 𝐶 )
14 simplr ⊢ ( ( ( 𝜑 ∧ 𝐵 = 𝐶 ) ∧ 𝑥 ∈ 𝐴 ) → 𝐵 = 𝐶 )
15 14 eqeq2d ⊢ ( ( ( 𝜑 ∧ 𝐵 = 𝐶 ) ∧ 𝑥 ∈ 𝐴 ) → ( 𝑥 = 𝐵 ↔ 𝑥 = 𝐶 ) )
16 15 ralrimiva ⊢ ( ( 𝜑 ∧ 𝐵 = 𝐶 ) → ∀ 𝑥 ∈ 𝐴 ( 𝑥 = 𝐵 ↔ 𝑥 = 𝐶 ) )
17 13 16 impbida ⊢ ( 𝜑 → ( ∀ 𝑥 ∈ 𝐴 ( 𝑥 = 𝐵 ↔ 𝑥 = 𝐶 ) ↔ 𝐵 = 𝐶 ) )