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\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.