My textbook says that it is clear that:
$\vdash \Gamma \cup \{\psi\}$ implies $\vdash \Gamma \cup \psi'$, where $\psi'$ is just $\psi$ with one of its bound variables renamed.
I am trying to show this for myself, but I find substitution/renaming/replacing more of a semantic idea than a syntactic one, can you show this formally?
For a semantic approach, by soundness, $\vdash \Gamma \cup \psi$ implies $\models \lor (\Gamma \cup \psi)$. So there is a model $M$ and an assignment $a$ so that $M\models (\lor (\Gamma \cup \psi))[a]$. So that $M \models \psi[a]$ or $M \models \sim \psi [a]$. From here, can I simply pass to another assignment $b$, where $b$ is the same as $a$ only different on the specific variable where $\psi$ and $\psi'$ differ, and climb back up with $M \models \psi'[b]$ or $M\models \sim \psi'[b]$ therefore $M \models \Gamma \cup \psi'$ and by completeness $\vdash \Gamma \cup \psi?$
Two issues I see with my proof:
1) The last step is not really completentess, copmleteness says $\Sigma \models \phi \rightarrow \Sigma \vdash \phi$, which is the converse of correctness, but here I'm using it as more of a converse to 'soundness'.
2) Passing to the assignment $b$ is unjustified, even though for some reason it doesn't feel wrong.
Hint
Note : I'll move $\Gamma$ to the left of $\vdash$ because the usual derivation relation holds between a set $\Gamma$ of formulas and a single formula $\psi$ (a derivation has zero or more premises and a single conclusion).
IMO; a complete proof must be on induction on the complexity of $\psi$, but the key-point is the base case that we can assume as : $\psi := \forall x \phi$.
I'll assume for simplicity that $\Gamma$ and $\psi$ are sentences.
From the derivation $\Gamma \vdash \psi$ we can easily manufacture the derivation $\Gamma \vdash \psi'$, where $\psi' := \forall z \phi(x/z)$, with $z$ new.
The details depend on the proof system: with Natural Deduction we have to use $(\forall \text E)$ and $(\forall \text I)$ rules, while with an Hilbert system we have to use the "typical" quantifier axiom : $\forall x \phi \to \phi(x/t)$ and the meta-theorem : $\Sigma \vdash \phi \text { iff } \Sigma \vdash \forall x \phi$.
For the Hilbert case, starting from : $\Gamma \vdash \forall x \phi$, we have to use the following instance of the quantifier axiom : $\vdash \forall x \phi \to \phi(x/z)$ with Modus Ponens to get : $\Gamma \vdash \phi(x/z)$.
Then use the instance of the meta-theorem : if $\Gamma \vdash \phi(x/z)$, then $\Gamma \vdash \forall z \phi(x/z)$ to get :
The symbol $\vdash \Gamma \cup \{ \psi \}$ probably means that you are working with a "Gentzen-style" proof system.
See e.g. Mordechai Ben-Ari, Mathematical Logic for Computer Science (Springer, 3rd ed. 2012), page 51-on, where we say that we can prove a set $U$ of formulas : $\vdash U$.
The proof is the same; if we have a proof-tree for $\vdash \Gamma \cup \{ \psi \}$ we can re-use the same proof-tree for $\vdash \Gamma \cup \{ \psi' \}$, where $\psi' := \forall z \phi(x/z)$.
When we have to "manage" the $\psi'$ formula, the rules for $\gamma$- and $\delta$- quantified formulas works "uniformly".
The result of deriving $\phi(z/a)$ from $\forall z \phi(x/z)$ is the same as that of deriving $\phi(x/a)$ from $\forall x \phi$.