In Lectures in Logic and Set Theory(Vol.2) by George Tourlakis, there is a metatheorem as follows:
I cannot see intuitively why the $x_1$ that occurs free in $A[e_1,...,e_n]$ does not matter. For example, let $A[e_1,...,e_n] \equiv x_1=e_1\rightarrow P(e_1, e_2)$, then $A[y_1,...,y_n] \equiv x_1=y_1\rightarrow P(y_1, y_2)$ and $A[x_1,...,x_n] \equiv x_1=x_1\rightarrow P(x_1, x_2)$. Doesn't the $x_1$ introduced in the final step interfere with the original one?
On
The issue is that there are no issues with the "identification" of free variables.
Consider the following simple example: $\Gamma \vdash \mathscr A(x,y)$.
Using Coroll.I.4.9 we have that $\Gamma \vdash \forall x \forall y \mathscr A(x,y)$, and thus (instantiating): $\Gamma \vdash \mathscr A(z,z)$.
Now, by a pair of similar moves, we get:
$\Gamma \vdash \mathscr A(x,x)$.
The key-point is convincing yourself (maybe semantically) that the above Corollary is sound.
The last boils down to $P(x_1,x_2)$, which looks like being too strong. However, we have to start from $\vdash_{\mathfrak T'}\mathscr A[e_1,e_2]$, but as $\Gamma'=\Gamma$, we cannot have used any special properties of the new names $e_1,e_2$ in deriving $\mathscr A[e_1,e_2]$. Put differently, when $x_1,x_2$ are free, we certainly have $\Gamma'\cup\{x_1=e_1,x_2=e_2\}\vdash_{\mathfrak T'}\mathscr A[x_1,x_2]$ and can translate any derivation of that into $\Gamma\vdash_{\mathfrak T}\mathscr A[x_1,x_2]$.