Power set

Set

context $X$ … set
definiendum $ Y \in \mathcal{P}(X) $
postulate $ Y\subseteq X $

Here we define

$\mathcal{P}(X) \equiv \{Y\mid Y\subseteq X\}$

which is sensible in our set theory if, for each set $X$, we have

$\exists! P.\,P = \{Y\mid Y\subseteq X\}$

or, more formally,

$\forall X.\,\exists! P.\,P = \{Y\mid Y\subseteq X\}$

which is short for

$\forall X.\,\exists! P.\,\forall Y.\,\left(Y\in P\Leftrightarrow Y\subseteq X\right)$

Discussion

The above is short for

$\forall X.\,\exists! P.\,\forall Y.\,\left(Y\in P\Leftrightarrow \forall Z.\,(Z\in Y\implies Z\in X)\right)$

and this is, apart from the exclamation mark,exactly the Axiom of power set.

Like in the case of the empty set, uniqueness follows from extensionality.

Examples

We can prove

$\forall Y.\,\left(Y\in \{\emptyset\}\leftrightarrow Y\subseteq \emptyset\right)$

Therefore, for $X$ being $\emptyset$, we can show that the job of $P$ is done by $\{\emptyset\}$. In other words

$\mathcal{P}(\emptyset)=\{\emptyset\}$
Remarks

Generally, $\emptyset\in\mathcal{P}(X)$ for any $X$. Hence no power set is empty.

One also writes $ \mathcal{P}(X) \equiv 2^X\equiv\Omega^X $.

Reference

Wikipedia: Axiom of power set


Context

Sets