I'm reading Mathematical Logic by Stephen Cole Kleene and I am stuck trying to understand the logic behind his rule of universal quantifier introduction.
In the text, for propositional and first-order logic, the author provides first a Hilbert-type system for deduction and then a Gentzen-type system. In the Hilbert-type system for first-order logic, he posits a universal quantifier rule, which is formulated as such:
If $C \to A(x)$
then $C \to \forall(x)A(x)$
where $C$ is a 0-place predicate/propositional variable/formula with no free variables
$A(x)$ is a unary predicate taking $x$/a formula with $x$ free
This rule is re-branded as universal quantifier introduction in the Gentzen-type system with syntax modified thus:
If $G \vdash A(x) $
then $G \vdash \forall(x)A(x)$
where $G$ is the set of assumptions with the requirement that $G$ does not contain $x$ free
and $A$ is as it was in the previous formulation
I can't seem to grasp the logic behind either formulation of this rule. It doesn't follow that $[C \to A(x)] \to [C \to \forall(x)A(x)]$ since $C$ could be true and $A$ could hold for $x$ but not for all $x$s, rendering the former implication true and the latter false which would immediately make the whole implication false. If any light could be shed on why this rule holds and maintains the soundness of the deduction, it would be much appreciated.