Universal generalization

In predicate logic, generalization (also universal generalization or universal introduction,GEN) is a valid inference rule. It states that if ${\displaystyle \vdash P(x)}$ has been derived, then ${\displaystyle \vdash \forall x\,P(x)}$ can be derived.

The full generalization rule allows for hypotheses to the left of the turnstile, but with restrictions. Assume Γ is a set of formulas, ${\displaystyle \varphi }$ a formula, and ${\displaystyle \Gamma \vdash \varphi (y)}$ has been derived. The generalization rule states that ${\displaystyle \Gamma \vdash \forall x\varphi (x)}$ can be derived if y is not mentioned in Γ and x does not occur in ${\displaystyle \varphi }$.

...
Wikipedia