DEF-P. Powerset.
The power set of $X$, denoted by $\mathcal{P}(X)$, is the unique set $Y$ such that
\[\forall y :\enspace y\in Y \enspace\Leftrightarrow\enspace y\subseteq X.\]The existence of $Y$ is justified by Axiom of Power Set and the uniqueness is justified by Axiom of Extensionality.
PROP-P-EMP.
\[\mathcal{P}(\varnothing) = \{\varnothing\}.\]