Why are the axiom of specification is an axiom schema? Why not just a single axiom?

This is just the choice of underlying logic. ZFC is a theory in first-order logic, and the strictures of that logical system rule out certain kinds of expressions. There are other logics, and their study comprises abstract model theory.

Very roughly, there are two competing hopes for a logical system:

• It should be expressive: things we intuitively want to be able to say, should be say-able in the system.

• It should be not too wild: e.g. there should be a well-behaved notion of proof.

It turns out that these are fundamentally in tension. For example, if we want proofs to be finite, then our logical system can't capture infinite structures up to isomorphism (this is the compactness theorem, essentially).

So why did we pick first-order logic after all, given that it forces us to use axiom schemata (and other inefficiencies)? Well, first-order logic seems to sit at a sweet spot here: it's fairly expressive, but also has a very well-behaved notion of proof and a more technical property called the "Lowenheim-Skolem property" which roughly says that it doesn't interact too much with set theory (indeed, it's the most expressive logic with these properties - this is due to Lindstrom).

This paper of Ferrairos may be of interest with regard to how first-order logic emerged as "the" primary logic of mathematics.

In ZF, all expressions must ultimately be a syntactically valid, finite combination of variable names, the $\forall$ quantifier, parentheses, the logical operations $\lnot$ and $\lor$, $=$ and finally $\in$. That's it.

Of course, in practice we have a lot of other symbols, like $\subseteq$ and $\exists$, but technically they are all defined as specific shorthands for combinations of the symbols above.

There is no way to use these to say $\forall \phi(\phi\text{ is a formula}\to\ldots)$, the way one might want to do to make the axiom schema into actual axioms.