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	$$⊢\phi \to B\in ℝ$$
	renegeulemv.1	$$⊢\phi \to \exists y\in ℝB+y=A$$
Assertion	renegeulem	$$⊢\phi \to \exists !y\in ℝB+y=A$$

Proof

Step	Hyp	Ref	Expression
1		renegeulemv.b	$$⊢\phi \to B\in ℝ$$
2		renegeulemv.1	$$⊢\phi \to \exists y\in ℝB+y=A$$
3	1 2	renegeulemv	$$⊢\phi \to \exists !x\in ℝB+x=A$$
4		reurex	$$⊢\exists !x\in ℝB+x=A\to \exists x\in ℝB+x=A$$
5	3 4	syl	$$⊢\phi \to \exists x\in ℝB+x=A$$
6	1 5	renegeulemv	$$⊢\phi \to \exists !y\in ℝB+y=A$$