EDB — 1Y1

[1Y1] The axiom of the power set says that for every set $A$, there is a set $\mathcal{P}(A)$ whose elements are all and only subsets of $A$. A shortened definition formula is

$\mathcal{P}(A)$ is also called set of parts.

In the formal language of the Zermelo-Fraenkel axioms, the axiom is written:

this formula implies that the power set $Z$ is unique, therefore we can denote it with the symbol $\mathcal{P}(A)$ without fear of misunderstandings.

Note that

can be shortened with $y\subseteq A$ and therefore the axiom can be written as

then using the extensionality, we obtain that