Lambda Calculus - free vs. bound variables
Iterated abstraction uses abstraction to the right:

\begin{align}
LHS
&amp;= (\quad \lambda wx.wx \space\space\space)\space(\lambda wx.wx) \\
&amp;= (\lambda w.(\lambda x.wx))\space(\lambda wx.wx)
\end{align}

The beta reduction axiom is $(\lambda x. M[x])N = M[x := N]$.

To satisfy your original equation, replace all occurences of $x$ in the beta reduction axiom, with $w$. Then, substitute the following values into the beta reduction axiom: $$M[w] = (\lambda x.wx)$$ $$N = (\lambda wx.wx)$$

The beta reduction axiom with substituted values is $$(\lambda w.(\lambda x .wx))(\lambda wx.wx) = M[w:=(\lambda wx.wx)]$$

where $M[w:=(\lambda wx.wx)]$ means "substitute all occurences of $w$ in $M$ with $(\lambda wx.wx)$". So we get:

$$(\lambda w.(\lambda x .wx))(\lambda wx.wx) = (\lambda x.(\lambda wx.wx)x)$$

as expected.

For the $(\lambda y.a)b \rightarrow a$ equation, $y$ is a bound variable, while $a$ is a free variable. We apply $b$ to all occurences of $y$, but there are none so our expression doesn't change (no $y$ is converted to $b$). The result is still $a$, unchanged.

Source, really well written and accessible if you give it enough time.