This question is about how accurate is it to say that axiomatic set theory is a first-order logic (FOL) theory? The crux of the matter is the nature of the set comprehension symbol $\{\_ \mid \_ \}$.
In FOL, the collection of non-logical symbols is parametric on a triple $(X,F,P)$ where $X$ is a collection of variables, $F$ a collection of function symbols, and $P$ is a collection of predicate symbols. For example, $\emptyset \in F$ represents the empty set and ${\subseteq} \in P$ represents the subset relation. Usually, axiomatic set theory is built from $X$ ranging over all collections, $F = \{\emptyset\}$ and $P = \{{\in},{=}\}$. So far so good.
However, is the binary symbol $\{\_ \mid \_ \}$ in $F$ or in $P$? On the one hand, it is intuitively a function symbol because it identifies a collection in the domain of discourse. However, the second argument in this symbol is a formula in the syntax of the theory ... and this sadly breaks the hierarchy for how terms in FOL are built: terms at the bottom in any syntax tree. On the other hand, one might say that it is a predicate symbol that, in the end, is meta-notation for succinctly writing a formula that uniquely identifies an object in the domain of discourse. However, the expressions $x \in \{ y \mid \phi \}$ and $x \in y$ (assuming $x,y \in X$ and $\phi$ a formula) uses differently the membership predicate symbol: in the former, it refers to the membership of $x$ in a formula!?!?; in the latter, it refers to the membership of $x$ in a collection.
So, which one is it? I have checked several axiomatic set theory books (including Kunen, Jech, and a few more) and there is no clear explanation that can help to answer my question. Btw, it is also OK if you point out that such an axiomatization for set theory, to begin with, is beyond the reach of FOL.
$\{\ \mid \ \}$ can also be seen as simply an abreviation, that does not appear in the "actual" formulas of set theory, just like $\subset$.
If the formula is $\forall x, x\subset y \implies P(x)$, then the actual formula should be $\forall x, (\forall z, z\in x\implies z\in y) \implies P(x)$.
Similary, if the formula is $P(\{x \in z\mid \phi(x)\})$, then the actual formula is $\forall y, y= \{x \in z\mid \phi(x)\} \implies P(y)$ where $y= \{x \in z\mid \phi(x)\}$ is an abreviation that stands for $ (\forall t, t\in y \implies (t\in z \land\phi(t)) )\land (\forall t, (t\in z\land \phi(t)) \implies t\in y)$, so $P(\{x \in z\mid \phi(x)\})$ is an abreviation for
$\forall y, ((\forall t, t\in y \implies (t\in z \land\phi(t)) )\land (\forall t, (t\in z\land \phi(t)) \implies t\in y)) \implies P(y)$.
Now since $ZF \vdash \exists ! y, y= \{x \in z\mid \phi(x)\}$, we allow ourselves to use the latter symbol as an abbreviation for a unique element.
Similarly, $\cup$ is not in the language of set theory, but we allow ourselves to write $A\cup B$ for a set since $ZF\vdash \exists ! z, z=A\cup B$ where $z= A\cup B$ is an abbreviation for a formula that I will let you write out if you wish.
So one can also see this symbol as simply an abbreviation