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

Proof

Step	Hyp	Ref	Expression
1		renegeulemv.b	⊢ ( 𝜑 → 𝐵 ∈ ℝ )
2		renegeulemv.1	⊢ ( 𝜑 → ∃ 𝑦 ∈ ℝ ( 𝐵 + 𝑦 ) = 𝐴 )
3	1 2	renegeulemv	⊢ ( 𝜑 → ∃! 𝑥 ∈ ℝ ( 𝐵 + 𝑥 ) = 𝐴 )
4		reurex	⊢ ( ∃! 𝑥 ∈ ℝ ( 𝐵 + 𝑥 ) = 𝐴 → ∃ 𝑥 ∈ ℝ ( 𝐵 + 𝑥 ) = 𝐴 )
5	3 4	syl	⊢ ( 𝜑 → ∃ 𝑥 ∈ ℝ ( 𝐵 + 𝑥 ) = 𝐴 )
6	1 5	renegeulemv	⊢ ( 𝜑 → ∃! 𝑦 ∈ ℝ ( 𝐵 + 𝑦 ) = 𝐴 )