How do we manipulate the universal quantifier (∀) in the course of a formal proof?

Two ways:

ELIMINATION is pretty easy: from ∀xP(x), infer P(c) for any constant c. (The basic idea is, if everything is P, and c names an object in our domain, then c is a P, too).

INTRODUCTION is tricky: take some arbitrary constant, e, not appearing elsewhere in the proof. Anything that holds of e holds of everything, since e is arbitrary. So if you can show that P(e) holds for this arbitrary object, you're entitled to infer that ∀xP(x).

The most important application of ∀-intro is general conditional proof: assuming P(e), show Q(e), and from there you can infer that every P is a Q, i.e. that ∀x(P(x) → Q(x)).