One of the rules for the definition of substitution in the lambda-calculus is:
$$[x \mapsto s]y = y \ \text{ if } \ x \neq y$$
But how can $x = y$? After all I am not substituting $y$ for $s$, but $x$.
I think I am just confused with the notation but it seems quite essential, so I really want to understand this thoroughly.
The question is subtle.
First, $[x \mapsto s]y$ stands for the term obtained from $y$ by replacing $x$ with $s$. So, I'm not a native English speaker but I would say that you are substituting $s$ for $x$ (in $y$) and not substituting $x$ for $s$.
Moreover, and most importantly for your question, $x$ and $y$ are meta-variables, i.e. are two (distinct) symbols that stand for two variables. It might happen that both symbols stand for the same variable (this is the case where $x = y$), so you have to take into account also that case (and clearly, $[x \mapsto s]y = s$ in that case).
When you define the language of the $\lambda$-calculus, you first fix a countably infinite set of variables. These variables are denoted by $x, y, z, \dots$ but are not $x, y, z, \dots$: indeed, $x, y, z, \dots$ are just symbols that stand for variables. This is the meaning of meta-variables.