In ZFC, a class is given by a class formula $\phi$, that is, a formula expressed in the language of ZFC. For example, the notion of group can be formalized by such a formula $\phi$. The notion of group homomorphism can also be so formalized, say by $\psi$. So in principle there is no problem in being able to write down a formula in ZFC whose abbreviation is

$$\exists 1 \ \forall G \ \phi(G) \Rightarrow \exists ! f \ \psi(f) \wedge dom(f) = G \wedge cod(f) = 1$$

and this is what you're after.

"Unbounded" quantification takes place all the time in ZFC. For example, the pairing axiom involves the formation of a set $\{x, y\}$ for any two sets $x, y$, and this "any" involves quantification over the class of sets. You do of course have to be careful around unbounded quantification, as we know from the classical set-theoretic paradoxes, but this is well worked out.

In ZFC, a class is given by a class formula $\phi$, that is, a formula expressed in the language of ZFC. For example, the notion of group can be formalized by such a formula $\phi$. The notion of group homomorphism can also be so formalized, say by $\psi$. So in principle there is no problem in being able to write down a formula in ZFC whose abbreviation is

$$\exists 1 \ \forall G \ \phi(G) \Rightarrow \exists ! f \ \psi(f) \wedge dom(f) = G \wedge cod(f) = 1$$

and this is what you're after.

"Unbounded" quantification takes place all the time in ZFC. For example, the pairing axiom involves the formation of a set $\{x, y\}$ for any two sets $x, y$, and this "any" involves quantification over the class of sets. The axioms of set theory should be formulated to avoid completely unbounded instances of say the comprehension or separation axiom, as we know from the classical set-theoretic paradoxes, but all this is well worked out.