Set existence axiom

Statement

In many formal set theories, such as Zermelo–Fraenkel set theory, set builder notation is not part of the formal syntax of the theory. Instead, there is a set existence axiom scheme, which states that if $E$ is a set and $\Phi(x)$ is a formula in the language of set theory, then there is a set $Y$ whose members are exactly the elements of $E$ that satisfy $\Phi$:

$$(\forall E)(\exists Y)(\forall x)[x \in Y \Leftrightarrow x \in E \land \Phi(x)].$$

The set $Y$ obtained from this axiom is exactly the set described in set builder notation as $\{ x \in E \mid \Phi(x)\}$.