In first-order logic typical rules governing the quantifiers are :
$${\Gamma \vdash \forall x \alpha \over \Gamma \vdash \alpha [x/t] }\, \, (\text{where} \, t \, \text{is substitutable for} \, x \text{in} \alpha)$$
$${\Gamma \vdash \alpha [x/y] \over \Gamma \vdash \forall x \alpha }\, \, (y \, \text{not free in} \, X \cup \alpha)$$
Thus, in your example, having proved :
$∀x[P(x) \rightarrow Q(x)]$
we can derive :
$P(t) \rightarrow Q(t)$
for every term $t$, included $x$ itself.
For the other "direction", if we have proved :
$\Gamma \vdash P(y) \rightarrow Q(y)$,
provided that $y$ is not free in any formula in $\Gamma$, we can conclude :
$\Gamma \vdash \forall x[P(x) \rightarrow Q(x)]$.
In the above proof $\Gamma$ is a set of formulae, and we can have $\Gamma = \emptyset$.
Thus, as a particular case of the above meta-theorem (usually called Generalization Theorem) we have :
if $\vdash \alpha[x/y]$, then $\vdash \forall x \alpha$.
The proviso is necessary in order to avoid fallacies.
If we assume $x = 0$, we can write the following derivation :
$x = 0 \vdash x = 0$;
from it, mis-applying the above rule [because $\Gamma = \{ x = 0 \}$ and $x$ is free in it]:
$x = 0 \vdash \forall x (x = 0)$.
By use of Deduction Theorem we can conclude :
$\vdash x = 0 \rightarrow \forall x (x = 0)$.
But this may not be because, by soundeness of first-order logic (i.e. : if $\vdash \alpha, then \vDash \alpha$) we expect that only valid formulae are provable, and the above formula is not valid.
Tho show that it is not, consider an interpretation with domain the set $\mathbb N$ of natural numbers and consider an assignement $s$ of value to the free variables [i.e. a function $s : Var \rightarrow \mathbb N$] such that $s(x)=0$.
Clearly :
$(x = 0 \rightarrow \forall x (x = 0))[s] = FALSE$
because $(x = 0)[s]$ is $0 = 0$, which is true, while $\forall x (x = 0)$ is false.