DEF-BLD. Set-Builder.
Let $X$ be a set and $\varphi(x,p)$ be a formula with free variables among $x$ and $p$. The notation
\[\{x\in X : \varphi(x,p)\}\]denotes the unique set $Y$ such that
\[\forall x :\enspace x\in Y \enspace\Leftrightarrow\enspace x\in X\land\varphi(x,p).\]The existence of $Y$ is justified by Separation Schema and the uniqueness is justified by Axiom of Extensionality.