In ZFC, the axiom of separation is given as follows.
Let $\phi(x, w_1,\ldots, w_n)$ be a wff formula in FOL, for free variables $w_1,\ldots,w_n$. Then, $$\forall w_1,\ldots,w_n\forall A \exists B\forall x(x\in B \iff (x\in A \wedge \phi(x,w_1,\ldots,w_n, A)))$$
It is trivially easy to prove within a formal system for any instantations of $A$ and $B$, $B\subseteq A$. Likewise, a proof outside of the formal system that this holds for any property $\phi$ is about as straightforward as well.
My question is this: Is this statement provable within ZFC, or would this be an example of an unprovable but true statement? At first glance, it looks to me that it would be unprovable, since a proof would seem to require you to quantify over $\phi$, which is not permitted in first order logic. If this is provable, what would a proof of this look like?
If you consider $\phi$ to be a variable, this is not even a statement in ZFC, because ZFC, as first-order theory, not only can't prove statements with quantifiers over predicates, but can't even formulate them.
If you substitute $\phi$ with some specific formula, then you get a statement. And the statement you get will be provable in ZFC. In fact it will be an axiom - one of axioms you get from schema of separation.