Why is alpha-equivalence in untyped $\lambda$-calculus substitutive?

I think this is proved in H. B. Curry and R. Feys. Combinatory Logic, Volume I. North-Holland Co., Amsterdam, Theorem 2a on page 95. The proof, with all the auxiliary results and some consequences, occupies pages 96-103.

This is addresses, for example, in A. Gordon and T. Melham's "Five Axioms of Alpha-Conversion". The use de Bruijn indices to get things done. If you can read Slovene, a student of mine has worked out all the nasty details directly in syntax.

For the sake of completeness, here is an answer using freely avaliable (online) sources:

Most of this question is actually answered in the first two sections of Chapter 1 of

Jean-Louis Krivine, Lambda-calculus, types and models, 22 January 2009. http://www.pps.jussieu.fr/~krivine/articles/Lambda.pdf . (This is a very good text, once you have accustomed to the suboptimal formatting.)

What little remains to be done is done at http://www.cip.ifi.lmu.de/~grinberg/mo65420.pdf . This PDF uses the notations of Krivine, but the last six lemmata (Lemmata 1.J-1.O) show that his definition of substitution is equivalent to mine, and that mine is actually well-defined.