How do I prove Separation Schema within ZFC?

The idea of a schema is to replace a second-order idea by a template for axioms. So the natural thing is to also have a template for a proof.

Different Separation axioms have different proofs, since mostly they rely on different Replacement axioms to be proven. But we have a recipe, a template, an algorithm, that given any axiom in the Separation schema, we can prove that axiom.

Since the whole debate here is meta-mathematical anyway, that quantification which happens in the meta-theory is just that. Or, if you will, if this wasn't the case, there would be some Separation axiom $\varphi$ which cannot be proved from $\sf ZFC$, but plugging it into our template does work. So that's not the case.

As for your other question, deriving a contradiction is merely a proof that $\exists x(x\neq x)$. It's a finite proof, there are finitely many axioms from $\sf ZFC+\phi$ appearing in it. One of these axioms, presumably is your $\phi$, but the rest are just a finite list of axioms from $\sf ZFC$.