Yes, it is all correct.
Lambda-calculus may be just taken as a formal system, with rules to be
However, it may be useful to try to understand intuitively why the
rules are what they are.
So the following is very informal and should be taken as an attempt at
Consider whether the following expressions are equivalent:
$y$ and $z$ : they are not equivalent because a substitution on $y$ has
no effect on $z$, and conversely. The variables $y$ and $z$ are free
variables. They stand for themselves, or for
whatever value is associated to them in an environment where you
evaluate the expression, or by a substitution. Changing a free
variable for another (it is not renaming in such a case) will change
what you get in the environment, or by applying a substitution (which
amounts to the same).
$\lambda y. (x\,y)$ and $\lambda z.(x\,z)$ : they are equivalent
via alpha conversion. When applied to the same argument, and more
generally when used in the same context, they will always give the
same result. The variables $y$ and $z$ are bound variables. Renaming
a bound variable can be done at any time,
independently of the context, without ever changing the behavior of
The renaming in your example $ \lambda y. (x\,y) [x:=y] = \lambda
z.(y\,z)$ is needed because the $y$ in the substitution is a free
variable (possibly taking a value in whatever environment or
substitution may be provided). Without the renaming, it would be
undistinguisable from the bound variable of the $\lambda$-abstraction
once the substitution is performed. To avoid that, the bound variable
is renamed, since renaming it does not matter.
Contrarily, in the expression $(x\,y)[x:=y]$, both occurences of $y$
stand for the same free variable $y$ in the current environment. There
is no reason to try distinguishing them.