From Type Theory and Formal Proof, An Introduction by Rob Nederpelt and Herman Geuvers:
Lemma 1.7.1 Let $M_{1} =_{\alpha} N_{1}$ and $M_{2} =_{\alpha} N_{2}$. Then also:
(1) $M_{1}N_{1} =_{\alpha} M_{2}N_{2}$,
(2) $\lambda x . M_{1} =_{\alpha} \lambda x . M_{2}$,
(3) $M_{1}[x := N_{1}] =_{\alpha} M_{2}[x := N_{2}]$.
Why does this hold? There does not seem to be a stated connection between $M_{1}$ and $M_{2}$ or $N_{1}$ and $N_{2}$.