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