Subset $x\subseteq y$, proper subset $x⊊y$, and the separation notation $\{z\in x:\phi (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 $\mathrm{\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⊊y$, when $x\subseteq y$ and $x\mathrm{\ne }y$.

Separation notation. Let $x$ be a set, $\phi (z,\bar{p})$ a formula and $\bar{p}$ parameters. The Axiom Schema of Separation: for each formula $\phi$, $\mathrm{\forall }\bar{p}\mathrm{\forall }x\mathrm{\exists }y\mathrm{\forall }z(z\in y\leftrightarrow (z\in x\wedge \phi (z,\bar{p})))$ supplies a set whose elements are exactly the elements $z$ of $x$ for which $\phi (z,\bar{p})$ holds, and The Axiom of Extensionality: $\mathrm{\forall }x\mathrm{\forall }y(\mathrm{\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:\phi (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:\phi (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 $⊊$ 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}(\mathrm{\varnothing })=\{\mathrm{\varnothing }\}$; $\mathrm{\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)=\mathrm{\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.