Fresh bound-variable renaming preserves truth

No binder in $\psi$ uses $z$, so substitution introduces no capture. At an assignment $s[z:=a]$, the free-for identity gives truth of $\psi [z\mathrm{/}y]$ exactly when $\psi$ is true at $s[z:=a][y:=a]$.

Since $z$ is absent from $\psi$, coincidence (as used in the free-for lemma) removes the update at $z$ when evaluating $\psi$. The last assignment therefore gives the same truth as $s[y:=a]$. Quantifying over the same $a\in M$ proves the claimed equivalence. Inner binders for $y$ were untouched by the raw substitution rule.

A finite set of variable indices is bounded in $\omega$, by induction over its finite listing and taking successive maxima. There is an index outside it, and the least such index is uniquely specified by the natural order. This proves the fresh-variable assertion without choosing from a family of sets.