In the PDF textbook "A Friendly Introduction to Mathematical Logic 2nd Edition" by Christopher C. Leary and Lars Kristiansen, page 53, the first quantifier inference rule (QR) is defined by the ordered pair $(\Gamma,\theta)$ such that $\Gamma=\{\psi\to\phi\}$ and $\theta=\psi\to(\forall x\phi)$ where $x$ is not free in the formula $\psi$ (note this is important). The book provides a proof of $\Gamma\vDash\theta$ on page 56, but I decided to give my own, very similar proof.
My proof goes as follows:
$$\Gamma\vDash\theta\iff(\psi\to\phi)\vDash[\psi\to(\forall x\phi)]$$
Let $\mathfrak{U}$ be some fixed, arbitrary interpretation. Thus, continuing forth,
$$(\psi\to\phi)\vDash[\psi\to(\forall x\phi)]\iff\mathfrak{U}\vDash(\psi\to\phi)\Rightarrow\mathfrak{U}\vDash[\psi\to(\forall x\phi)]$$
If $\mathfrak{U}\not\vDash(\psi\to\phi),$ then we're done, so let's assume $\mathfrak{U}\vDash(\psi\to\phi)$ which we'll donote (Assumption 1). This leaves us to prove $\mathfrak{U}\vDash[\psi\to(\forall x\phi)]$ under (Assumption 1).
$$\mathfrak{U}\vDash[\psi\to(\forall x\phi)]\iff\mathfrak{U}\vDash\psi\Rightarrow\mathfrak{U}\vDash(\forall x\phi)$$
Like previously, if $\mathfrak{U}\not\vDash\psi$, then we're done, so let's assume $\mathfrak{U}\vDash\psi$ which we'll denote (Assumption 2). This leaves us to prove $\mathfrak{U}\vDash(\forall x\phi)$ under (Assumption 2).
\begin{align} \mathfrak{U}\vDash(\forall x\phi)&\iff(\forall s)(\mathfrak{U}\vDash(\forall x\phi)[s]) \\ &\iff(\forall s)(\forall a)(\mathfrak{U}\vDash\phi[s[x|a]]) \\ \text{Let $s=t$ be some fixed, arbitrary} \\ \text{variable assignment function into $\mathfrak{U}$.} \\ &\iff(\forall a)(\mathfrak{U}\vDash\phi[t[x|a]]) &&(1) \end{align}
From (Assumption 1),
\begin{align} \mathfrak{U}\vDash(\psi\to\phi)&\iff\mathfrak{U}\vDash\psi\Rightarrow\mathfrak{U}\vDash\phi \\ &\iff(\forall s)(\mathfrak{U}\vDash\psi[s])\Rightarrow(\forall s)(\mathfrak{U}\vDash\phi[s]) \\ \text{Let $s=t[x|a]$ be the same x-modified} \\ \text{assignment function seen in (1).} \\ &\iff\mathfrak{U}\vDash\psi[t[x|a]]\Rightarrow\mathfrak{U}\vDash\phi[t[x|a]]) \\ &\iff(\forall a)(\mathfrak{U}\vDash\psi[t[x|a]])\Rightarrow(\forall a)(\mathfrak{U}\vDash\phi[t[x|a]]) && (2) \end{align}
From (Assumption 2),
\begin{align} \mathfrak{U}\vDash\psi&\iff(\forall s)(\mathfrak{U}\vDash\psi[s]) \\ \text{Let $s=t[x|a]$ be the same x-modified} \\ \text{assignment function seen in (1).} \\ &\iff\mathfrak{U}\vDash\psi[t[x|a]] \\ &\iff(\forall a)(\mathfrak{U}\vDash\psi[t[x|a]])&&(3) \end{align}
Frome (2) and (3), we can deduce (1) and thus we have proven $\mathfrak{U}\vDash(\forall x\phi)$ and we are done. (I have left out some of the final steps, but the remaining steps should be trivial to complete from here hopefully.) $\square$
I'm pretty sure this proof is correct, but the only thing I'm unsure about is the necessity that $x$ be not free in $\psi$. The proof shown in the book uses this fact to help prove $\Gamma\vDash\theta$, so it makes me uneasy about the validity of my proof. From my proof, it seems unnecessary that $x$ be not free in the $\psi$, but I'm might be missing something. Can someone show me where I'm mistaken within my proof and explain why $x$ must not be free in $\psi$.