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	|- ( ph -> B e. RR )
	renegeulemv.1	|- ( ph -> E. y e. RR ( B + y ) = A )
Assertion	renegeulem	|- ( ph -> E! y e. RR ( B + y ) = A )

Proof

Step	Hyp	Ref	Expression
1		renegeulemv.b	|- ( ph -> B e. RR )
2		renegeulemv.1	|- ( ph -> E. y e. RR ( B + y ) = A )
3	1 2	renegeulemv	|- ( ph -> E! x e. RR ( B + x ) = A )
4		reurex	|- ( E! x e. RR ( B + x ) = A -> E. x e. RR ( B + x ) = A )
5	3 4	syl	|- ( ph -> E. x e. RR ( B + x ) = A )
6	1 5	renegeulemv	|- ( ph -> E! y e. RR ( B + y ) = A )