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

Metamath Proof Explorer

Theorem renegeulem

Description: Lemma for renegeu and similar. Remove a change in bound variables from renegeulemv . (Contributed by Steven Nguyen, 28-Jan-2023)

Ref Expression
Hypotheses renegeulemv.b ⊢ φ → B ∈ ℝ
renegeulemv.1 ⊢ φ → ∃ y ∈ ℝ B + y = A
Assertion renegeulem ⊢ φ → ∃! y ∈ ℝ B + y = A

Proof

Step Hyp Ref Expression
1 renegeulemv.b ⊢ φ → B ∈ ℝ
2 renegeulemv.1 ⊢ φ → ∃ y ∈ ℝ B + y = A
3 1 2 renegeulemv ⊢ φ → ∃! x ∈ ℝ B + x = A
4 reurex ⊢ ∃! x ∈ ℝ B + x = A → ∃ x ∈ ℝ B + x = A
5 3 4 syl ⊢ φ → ∃ x ∈ ℝ B + x = A
6 1 5 renegeulemv ⊢ φ → ∃! y ∈ ℝ B + y = A