# Definition of renaming in lambda calculus

From "Type Theory and Formal Proof, An Introduction" by Rob Nederpelt and Herman Geuvers:

Definition 1.5.1 (Renaming; $$M^{x \to y}$$; $$=_{\alpha}$$) Let $$M^{x \to y}$$ denote the result of replacing every free occurrence of $$x$$ in $$M$$ by $$y$$. The relation 'renaming', expressed with symbol $$=_{\alpha}$$, is defined as follows: $$\lambda x . M =_{\alpha} \lambda y . M^{x \to y}$$, provided that $$y \notin FV(M)$$ and $$y$$ is not a binding variable in $$M$$.

$$FV$$ denotes the set of free variables of a $$\lambda$$-term.

Are the conditions $$y \notin FV(M)$$ and $$y$$ is not a binding variable in $$M$$, the same as requiring that $$y$$ does occur in $$M$$? My understanding is that an occurrence of a variable can be either free, bound, or binding. If an occurrence of $$y$$ is bound in $$M$$, does this not also require that $$y$$ is a binding variable in $$M$$?