If set theory only contains the notions of “set” and “is a member of” as primitives, how can an axiom of set theory refer to a “formula”?

Question

It's said that the primitive concepts of set theory are those of "set" and "membership", then all axioms of set theory must begin with "Let $A$ be a set" or "Let $x\in A$", but they don't. For example, let us consider the subset axiom:

Subset Axiom. Let $\varphi(x)$ be a formula and let $A$ be a set. Then there exists a set $S$ such that for all sets $x$ we have that $x\in S$ if and only if $x\in A$ and $\varphi(x)$.

This axiom begins with "Let $\varphi(x)$ be a formula" but "formula" is not a primitive concept, then, for having sense, it must be a defined concept, but as far as I see we can't define "formula" in terms of "set" and "membership" if I am wrong, please tell me. Now, in the case where we can't define "formula", how is the subset axiom justified from a logical point of view?

In many books, when the subset axioms is introduced, the statement "Let $\varphi(x)$" is used informally, I will appreciate if you recommend me a book on set theory where the concept of "formula" is used formally, where there is a formal definition of what a formula is.

Thank you for your reading.

Answer 1

In formalizations of set theory (e.g. ZFC), this subset axiom you've described in usually called the axiom schema of specification. Note the use of the word "schema" in its name: this is where your confusion stems from. Indeed, formally speaking, this is not a single axiom, but a whole collection of axioms: one for every formula $\phi(x)$. For every formula $\phi(x)$, there is an axiom of set theory which goes "$\forall A \exists S \forall x (x \in S \Leftrightarrow (x \in A \wedge \phi(x)))$". Taken together, all these axioms make up what you call the subset axiom.

Edit: Axiomatic set theory is based on first-order logic, which is the system of language and inferences that are used to do this sort of math. It starts with symbols (including variables, connectives like $\neg$ and $\wedge$, quantifiers $\forall$ and $\exists$, the $=$ symbol, and predicate symbols) which are combined according to certain rules to make formulas. First-order logic also uses rules of inference to deduce some formulas from others. Set theory uses first-order logic with the predicate symbol $\in$; its axioms and theorems are formulas. I suggest reading some more (on Wikipedia or in your favorite textbook) if you're interested in learning more about how first-order logic works.

Answer 2

Formulas and first-order logic come "below" set theory, in that axiomatic set theories such as ZFC rest on top of first-order logic. In each language of first-order logic, there is a definition for what a formula is, which is a string of characters $($, $)$, $\land$, $\lnot$, $\lor$, variable symbols, relation symbols, and predicate symbols, which follows the rules for being a wff of that logic. But this is conceptually "below" set theory, and more general, as it also applies for formalizing what a formula is w.r.t. some other axiomatic systems like Peano arithmetic, or the group axioms.

About set theory resting on FOL, this answer sounds relevant.