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

Metamath Proof Explorer

Theorem renegeulemv

Description: Lemma for renegeu and similar. Derive existential uniqueness from existence. (Contributed by Steven Nguyen, 28-Jan-2023)

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

Proof

Step Hyp Ref Expression
1 renegeulemv.b ⊢ φ → B ∈ ℝ
2 renegeulemv.1 ⊢ φ → ∃ y ∈ ℝ B + y = A
3 simprl ⊢ φ ∧ y ∈ ℝ ∧ B + y = A → y ∈ ℝ
4 simplrr ⊢ φ ∧ y ∈ ℝ ∧ B + y = A ∧ x ∈ ℝ → B + y = A
5 4 eqcomd ⊢ φ ∧ y ∈ ℝ ∧ B + y = A ∧ x ∈ ℝ → A = B + y
6 5 eqeq2d ⊢ φ ∧ y ∈ ℝ ∧ B + y = A ∧ x ∈ ℝ → B + x = A ↔ B + x = B + y
7 simpr ⊢ φ ∧ y ∈ ℝ ∧ B + y = A ∧ x ∈ ℝ → x ∈ ℝ
8 simplrl ⊢ φ ∧ y ∈ ℝ ∧ B + y = A ∧ x ∈ ℝ → y ∈ ℝ
9 1 ad2antrr ⊢ φ ∧ y ∈ ℝ ∧ B + y = A ∧ x ∈ ℝ → B ∈ ℝ
10 readdcan ⊢ x ∈ ℝ ∧ y ∈ ℝ ∧ B ∈ ℝ → B + x = B + y ↔ x = y
11 7 8 9 10 syl3anc ⊢ φ ∧ y ∈ ℝ ∧ B + y = A ∧ x ∈ ℝ → B + x = B + y ↔ x = y
12 6 11 bitrd ⊢ φ ∧ y ∈ ℝ ∧ B + y = A ∧ x ∈ ℝ → B + x = A ↔ x = y
13 12 ralrimiva ⊢ φ ∧ y ∈ ℝ ∧ B + y = A → ∀ x ∈ ℝ B + x = A ↔ x = y
14 reu6i ⊢ y ∈ ℝ ∧ ∀ x ∈ ℝ B + x = A ↔ x = y → ∃! x ∈ ℝ B + x = A
15 3 13 14 syl2anc ⊢ φ ∧ y ∈ ℝ ∧ B + y = A → ∃! x ∈ ℝ B + x = A
16 2 15 rexlimddv ⊢ φ → ∃! x ∈ ℝ B + x = A