Subset $x \subseteq y$, proper subset $x \subsetneq y$, and the separation notation $\{\, z \in x : \varphi(z) \,\}$

For sets $x$ and $y$ we write $x \subseteq y$, and say that $x$ is a subset of $y$ or that $x$ is included in $y$, for the formula $\forall t\,(t \in x \to t \in y)$ of the language of set theory (The first-order language of set theory: $\in$, $=$, formulas with parameters, and class abbreviations); thus $x \subseteq y$ means that every element of $x$ is an element of $y$. We also write $y \supseteq x$ for $x \subseteq y$.

$x$ is a proper subset of $y$, written $x \subsetneq y$, when $x \subseteq y$ and $x \neq y$.

Separation notation. Let $x$ be a set, $\varphi(z,\bar p)$ a formula and $\bar p$ parameters. The Axiom Schema of Separation: for each formula $\varphi$, $\forall \bar p\,\forall x\,\exists y\,\forall z\,(z \in y \leftrightarrow (z \in x \wedge \varphi(z,\bar p)))$ supplies a set whose elements are exactly the elements $z$ of $x$ for which $\varphi(z,\bar p)$ holds, and The Axiom of Extensionality: $\forall x\,\forall y\,(\forall z\,(z \in x \leftrightarrow z \in y) \to x = y)$ shows there is only one such set. It is written

$\{\, z \in x : \varphi(z,\bar p) \,\}$

and every set introduced on this page by separating a condition inside a set already in hand is written this way. Directly from the definition, $\{\, z \in x : \varphi(z,\bar p) \,\} \subseteq x$.

• $\subset$ is not used in this library. Sources disagree about it: some write $\subset$ for inclusion and some for proper inclusion, so a formula containing it cannot be read without knowing which convention its author used. $\subseteq$ and $\subsetneq$ are unambiguous and are the only two symbols used here.

• Membership and inclusion are different relations. $t \in x$ says $t$ is one of the elements of $x$; $t \subseteq x$ says every element of $t$ is an element of $x$. Neither implies the other in general, and $\mathcal{P}(\varnothing) = \{\varnothing\}$; $\varnothing \in \mathcal{P}(a)$ and $a \in \mathcal{P}(a)$; $a \subseteq b$ if and only if $\mathcal{P}(a) \subseteq \mathcal{P}(b)$; $\bigcup \mathcal{P}(a) = a$; $\bigcap \mathcal{P}(a) = \varnothing$; and $\mathcal{P}(a \cap b) = \mathcal{P}(a) \cap \mathcal{P}(b)$ while only $\mathcal{P}(a) \cup \mathcal{P}(b) \subseteq \mathcal{P}(a \cup b)$ holds is where the two are systematically related.