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 ⊢ ( 𝜑 → 𝐵 ∈ ℝ )
renegeulemv.1 ⊢ ( 𝜑 → ∃ 𝑦 ∈ ℝ ( 𝐵 + 𝑦 ) = 𝐴 )
Assertion renegeulemv ( 𝜑 → ∃! 𝑥 ∈ ℝ ( 𝐵 + 𝑥 ) = 𝐴 )

Proof

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