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 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | renegeulemv.b | ||
2 | renegeulemv.1 | ||
3 | 1 2 | renegeulemv | |
4 | reurex | ||
5 | 3 4 | syl | |
6 | 1 5 | renegeulemv |