Every source I've found so far says that first order logic is sufficient for defining ZFC set theory.
My lecture notes write the Axiom of Comprehension as follows:
For any formula $\phi(x)$ with parameters and any set $y$, there exists a set $z$ whose elements are precisely those elements $x$ of $y$ that satisfy $\phi(x)$.
Does this first bit "for any formula $\phi(x)$" require second order logic? If so, why do people say first order is sufficient for ZFC? If not, is this just a metalinguistic use of "for any" and not "$\forall$"? What are the advantages in that case of deciding we'll use first order logic anyway (if not that it's weaker?)