I have a question regarding this formulation of the Separation Axiom:
I quote from the Book "Handbook of Mathematical Logic", the chapter from which this is taken could also be found here.
Now we can turn to the axioms. The first point in our analysis was that a set is entirely determined by its members. This is the content of our first axiom.
Extensionality Axiom: $\forall z(z \in x \leftrightarrow z \in y) \rightarrow x = y$.
One of th most important points established by our analysis is that certain collections of sets are sets. In translating this into our language, we face a difficulty: there is no general method of talking about collections in this language before we know that they are sets. There are, however, certain collections which we can talk about. Given a formula $\phi(x)$, we can say certain things about the collection of all sets $x$ such that $\phi(x)$. In particular, we can say that it is a set as follows: $\exists y \forall x(x \in y \leftrightarrow \phi(x))$. We abbreviate this expression to $Set\{ x : \phi(x) \}$. Our first principle of set existence is: if every member of a collection of sets belongs to the set $x$, then that collection is a set. To see this, suppose that $x$ is formed at state $S$ [...]
Separation Axiom: $\forall x (\phi(x) \to x \in y) \to Set\{ x : \phi(x) \}$.
For what is the term $\forall x (\phi(x) \to x \in y)$ in the Separation Axiom, wouldn't it be sufficient to just state $Set\{ x : \phi(x) \}$ i.e. the formulae $\exists y \forall x(x \in y \leftrightarrow \phi(x))$ as the Separation Axiom?
The Separation Axiom tells us that certain "definable" collections are sets. In particular, this form tells us that "definable" subfamilies of sets are themselves sets. The subformula $\forall x ( \phi (x) \rightarrow x \in y )$ is there to limit the Axiom to produce only subfamilies of collections that are already known to be sets. Without this condition it would be possible to use this form of the Axiom to conclude that $$\{ x : \neg ( x \in x ) \}$$ is a set, which is Bertrand Russell's famous paradox. Together with the condition we can only conclude that given any set $y$ the collection $$\{ x : x \in y \wedge x \notin x \}$$ is a set, from which we do not obviously derive a contradiction. (Usually this is used to prove the existence of the empty set $\varnothing$.)
Often this axiom (schema) takes a slightly different form:
This form essentially tells us that collections of the form $\{ x \in y : \phi(x) \} = \{ x : x \in y \wedge \phi (x) \}$ are sets (whenever $y$ itself is a set).