Universal generalization rule ($\Gamma ⊢\phi ⟹\Gamma ⊢\forall x\phi$)

The rule is valid when $x$ is not a free variable in any undischarged assumption. Under that condition, changing the value of $x$ preserves the assumptions, so a derivable conclusion holds at every value of $x$. Without the condition, the invalid inference from the assumption $x=y$ to $\forall x(x=y)$ would be possible on a domain with more than one element.