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