[[!redirects Sandbox > history]] [[!redirects Sandbox]] < [[nlab:Sandbox]] Structure: 1. A primitive binary relation $\in$ representing membership 2. A primitive binary relation $=$ representing equality 3. A primitive constant $\emptyset$ representing the empty set. 4. A primitive binary operation $(-,-)$ representing pairs of sets. 5. A primitive unary operation $U$ representing the union of sets. 6. A primitive unary operation $\mathcal{P}$ representing power sets. 7. A primitive constant $\mathbb{N}$ representing the natural numbers, a primitive constant $0$ representing zero, and a primitive unary operation $s$ representing successor. Axioms: 1. [[axiom of extensionality|Extensionality]]: for any set $x$ and $y$, $x = y$ if and only if for all $z$, $z \in x$ if and only if $z \in y$. 2. [[empty set|Empty set]]: for all sets $a$ and $b$, $a \in \emptyset$ implies $a \in b$. 3. [[axiom of ordered pairing|Ordered pairing]]: for all sets $a$, $a'$, $b$, and $b'$, $(a, b) = (a', b')$ if and only if $a = a'$ and $b = b'$. 4. [[axiom of union|Unions]]: for all sets $a$ and $c$, if $a \in U(c)$, then there exists $b$ such that $a \in b$ and $b \in c$, and for all $b$, if $a \in b$ and $b \in c$, then $a \in U(c)$. 5. [[axiom of power sets|Power sets]]: for all sets $b$, and $c$, if for all sets $a$, $a \in b$ implies $a \in c$, then $b \in \mathcal{P}(c)$. 6. [[axiom of infinity|Infinity]]: for all sets $x$, $s(x) \neq 0$ and $x \in \mathbb{N}$ if and only if $x = 0$ or there exists a set $y \in \mathbb{N}$ such that $s(y) = x$. 7. [[axiom of choice|Choice]]: for any set $a$, if for all $x \in a$ there is a set $y \in x$, then there is a function $f$ from $a$ to $U(a)$ such that $f(x) \in x$ for all $x \in a$. category: redirected to nlab