Definable power set
= Definable power set
{title2=$\mathcal D(X)$}
The definable power set $\mathcal D(X)=\operatorname{Def}(X)$ consists of the <subsets> of $X$ definable over the <first-order structure> $(X,\in)$ by a <first-order formula> with parameters from $X$. <Satisfaction for a set structure> makes this a definable operation in <ZF>. Iterating it produces the <constructible hierarchy> and the <relative constructible hierarchy>; their unions are the <constructible universe> and the <relative constructible universe>.