Wikipedia describes the first-order vs. second-order logic as follows:
First-order logic uses only variables that range over individuals (elements of the domain of discourse); second-order logic has these variables as well as additional variables that range over sets of individuals.
It gives $\forall P\,\forall x (x \in P \lor x \notin P)$ as an SO-logic formula, which makes perfect sense to me.
However, in a post at CSTheory, the poster claimed that $\forall x\forall y(x=y\leftrightarrow\forall z(z\in x\leftrightarrow z\in y))$ is an FO formula. I think this must not be the case, since in the above formula, $x$ and $y$ are sets of individuals, while $z$ is an individual (and therefore this must be an SO formula).
I mentioned this as a comment, but two users commented that ZF can be entirely described by FO logic, and therefore $\forall x\forall y(x=y\leftrightarrow\forall z(z\in x\leftrightarrow z\in y))$ is an FO formula.
I'm confused. Could someone explain this please?