Is the notation for the definition of a set stricly formalized?

First let me reveal a little secret about set theorists, and mathematicians in general: we hate complicated notations. We define different objects in different ways, but we then abuse the notation to ease the readability. It takes time to get used to, yes, but then it gets better.

First note that this is only a notation, if we agree from the beginning that either of these notational conventions mean the same thing, then they indeed mean the same thing. It is possible (and likely, and also true) that sometimes it makes more sense to use one notation and at other times to use the other one.

Second this is indeed a formula, but this is what we call a bounded formula. We bound ourselves to $X$. This often appears in explicit sentences (and formulae) as:

• $(\exists x\in X)\varphi(x)$ which really means: $\exists x(x\in X\land\varphi(x))$, or in universal versions:
• $(\forall y\in Y)\psi(y)$ which really means: $\forall y(y\in Y\rightarrow\psi(y))$.

As you can see it saves up both space and improves the readability, especially when there are three quantifiers or more.

Lastly, sets are classes. Recall that a class is a collection defined by a first order formula, but this formula is allowed to have parameters. So $X=\{v\mid v\in X\}$. Not all classes are sets, but all sets are indeed classes. This is why we often use $\{x\in X\colon\varphi(x)\}$, or $\{x\colon x\in X\land\varphi(x)\}$. It tells us that the collection is a subclass of $X$ and if $X$ is a set then this collection is also a set.

To close this, I'll add a remark that one of my most pedantic teachers told me that he sat a long time ago to verify that you can syntactically add the $\{\ldots\}$ to the language and all that. I cannot recall whether he left it undone; tried to retrace his proof a few years after and then left it undone; or originally tried to retrace the proof given by his teacher and left it undone.