---
tag: CP81H8276Z
kind: statement
role: proposition
name: Set existence axiom
sources:
  - wikipedia: en:220089@r1368739220
    locator: Set-builder notation, section Set existence axiom
    note: adopted
    mention: wikipedia://en/220089#IESX
    sections: [Statement]
inventory: [FB4JJ81R86]
---

## Statement

In many formal set theories, such as [[Zermelo–Fraenkel set theory|0HE5WDQ9FJ]], 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)\}$.