The other answers have explained that these axiom schemas of ZFC have to be schemas and not axioms, because we want ZFC to be a first-order theory. The reasoning is that we need to quantify over all formulae over ZFC. In particular, the Specification schema of ZFC can be stated as:
For each $(k+1)$-parameter sentence $φ$, ZFC has the axiom:
$∀p[1..k]\ ∀A\ ∃B\ ∀x\ ( x∈B ⇔ x∈A ∧ φ(p[1..k],x) )$.
Notice that we cannot have a single axiom that quantifies over all parametrized sentences (over the theory itself), because that is not (directly) expressible in first-order logic. In fact, it can be shown that ZFC cannot be finitely axiomatized (using the same language).
But that is not quite the full story. There is a general procedure to convert any sufficiently nice first-order theory $T$ into another first-order theory $T'$ (with a different language) that interprets $T$ and yet is finitely axiomatized. Doing this to PA yields a well-known second-order theory called ACA0, and doing this to ZFC yields almost NBG.
The basic idea to use two sorts, one sort $I$ for the original domain of $T$, and the other sort $J$ for 'classes', where each class is a subcollection of $I$ that represents some predicate over $T$. (For this, we need $T$ to support some reasonable ordered-pair encoding.) We then axiomatize the existence of the class of all objects in $I$, namely $∃C∈J\ ∀x∈I\ ( x∈C )$, which for convenience we shall state as existence of the class $\{ x : x∈I \}$. We also axiomatize the existence of the class $\{ (x,x) : x∈I \}$ to capture equality, and the existence of a class to capture each predicate/function-symbol of $T$. For example, to capture "$∈$" of ZFC we would have the class $\{ (x,y) : x,y∈I ∧ x∈y \}$. We also axiomatize existence of the singleton class $\{x\}$ for any $x∈I$, and that classes are closed under complement, union, intersection, cartesian product and projection.
If $T$ had finitely many predicate/function symbols, then the above axioms are finitely many, and yet allow us to construct any definable class of tuples over $T$, namely $\{ x[1..k] : φ(x[1..k]) \}$ for any $k$-parameter sentence $φ$ over $T$, as a member of $J$. Furthermore, every class that we can explicitly construct corresponds to some parametrized sentence over $T$. Thus we can now express any axiom schema of $T$ that quantifies over all parametrized sentences over $T$ as a single axiom quantifying over all members of $J$, and can prove that the resulting theory $T'$ is conservative over $T$ in the specific sense that every sentence over $T$ is provable by $T$ iff its translation (i.e. restricting every quantifier to $I$) is provable by $T'$.
Since any many-sorted first-order theory can be easily interpreted by a one-sorted first-order theory (i.e. replacing the sorts by predicate-symbols), it is inconsequential that we used two sorts in $T'$.
Quite apart from the finite axiomatizability of NBG, some set theorists prefer to say that they are working in NBG rather than ZFC, since it intrinsically allows definition and quantification over classes. But if one wants to be able to define a class whose defining formula involves quantifying over classes (like one can in ZFC define a set whose defining formula can quantify over sets), then the result (MK) is again is no longer finitely axiomatizable (in the language of NBG), because you would need an axiom schema for Specification of classes.