Wikipedia's article on universal generalization doesn't seem to give a satisfactory explanation of the restrictions on when it can be used:
Assume $\Gamma$ is a set of formulas, $\varphi$ a formula, and $\Gamma \vdash \varphi(y)$ has been derived. The generalization rule states that $\Gamma \vdash \forall x \varphi(x)$ can be derived if $y$ is not mentioned in $\Gamma$ and $x$ does not occur in $\varphi$.
The article then gives an example of UG being used incorrectly to derive $\exists z\exists w(z\neq w) \vdash \forall x(x\neq x)$, with the restrictions given certainly being violated. However, wouldn't the following modification of the "proof" be in accordance with the restrictions?
$\exists z\exists w(z\neq w)$
$\exists w(y\neq w)$
Here, the generalization in step 4 has been amended to use $\alpha$ as the quantifier's bound variable, which should be permitted, as $\alpha$ does not occur in $y\neq x$ and $y$ does not occur in the assumption $\exists z\exists w(z\neq w)$, yet this leads to a universal instantiation that is clearly false! Is the $\Gamma$ of the restrictions meant to be all previous steps of the proof, not just the assumptions? If so, wouldn't this invalidate the proof given further in the article that includes the steps $P(y)\to Q(y)$ and $P(y)$ before generalizing $Q(y)$? Does the presence of existential instantiation place further restrictions on universal generalization somehow, with the existential instantiated counting as a mention of the variable introduced?