Universal generalization rule
= Universal generalization rule
{title2=$\Gamma\vdash\varphi\Longrightarrow\Gamma\vdash\forall x\varphi$}
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.