The formal rule ∀Intro works just like Universal Generalization (UG).
The new device we need is how to declare that a name is arbitrary. We’ll do it by putting the name in square brackets in a subproof: [a]. We then end that subproof by proving that a has some property, which allows us to infer on the parent proof that the same holds ∀x. We cite the whole subproof with the arbitrary [a].
Here’s an example.
When we make “a” arbitrary with [a], we must put it in a subproof and justify it with Assume.
The other key fact about arbitrary names is that, when a name is arbitrary, it cannot appear anywhere outside the subproof. For example, it cannot appear in any of the premises or conclusion.
When we make the inference with ∀x, we must replace all the occurrences of xs with a.
If the name “a” does appear in a premise, and you need an arbitrary name, then just choose the next free letter in the alphabet.