Is it "legal" to switch $\forall x$ with $\forall s\forall t$? In the book The Foundations of Mathematics by Kenneth Kunen, in a chapter about set theory formalizations, the following first order logic sentence is provided (referred to as the Axiom of Comprehension/Separation Schema):
$\forall z \Big (\exists y \color{red}{\forall x} \big ( \color{red}{x} \in y \leftrightarrow x \in z \land \varphi(\color{red}{x}) \big ) \Big )$. I have colored in $\color{red}{\text{red}}$ the variable that I will be focusing on for the remainder of this question.
Consider the following two sets:
$A = \{ x \in \mathbb N \ |\  x \lt 5\}$.
$B = \{ \langle s, t \rangle \in \mathbb N \times \mathbb N \ |\ s \lt 5 \land t\lt 4 \}$

Now, let's say I wanted to look at set $A$ and confirm that it exists through the perspective of the Axiom of Comprehension Schema:
$\exists y \forall x (x \in y \ \leftrightarrow \ x \in \mathbb N \land x \lt 5)$ where $\varphi(x):= x \lt 5$. Cool. Set A exists.
To confirm set $B$'s existence, however, I run into an issue when it comes to inserting the predicate $\varphi$:
$\exists y \forall x (x \in y \ \leftrightarrow \ x \in \mathbb N \times \mathbb N \ \land \text{something} )$
I use the phrase "$\text {something}$" because "$\varphi (x)$" does not appear to decompose correctly into a statement about two variables...i.e. $\varphi(x)$ cannot be used to represent "$s \lt 5 \land t \lt 4$" because $s$ and $t$ are not necessarily equal, and therefore do not represent one object $x$.

A quick fix seems to be to switch $\forall x$ with $\forall s \forall t$ in order to generate the following statement:
$\exists y \forall s \forall t (\langle s,t \rangle \in y \ \leftrightarrow \ \langle s,t \rangle \in \mathbb N \times \mathbb N \ \land s \lt 5 \land t \lt 4  )$
I am uncertain why this is something that is allowed. Specifically, this seems to suggest that $\forall x  \ \varphi(x)$ is 'semantically' (regular English definition) equivalent to $\forall s \forall t \ \varphi (s,t)$.
From what I understand about first order logic, $\forall x \ \varphi (x)$ essentially means "For all singular objects in the domain of discourse, the following sentence about a singular object is true". Comparatively, I interpret $\forall s \forall t \ \varphi(s,t)$ as saying "For any two objects in the domain of discourse, the following sentence is true about two objects".
Is the syntax "$\ s,t\ $" a singular object in the domain of discourse? It doesn't strike me as one...hence my confusion.
Any input is greatly appreciated! Thank you.
 A: You use the projection functions - or rather, the projection relations. These are the binary relations $\pi_0(x,y)$ and $\pi_1(x,y)$, which we read as "$x$ is an ordered pair with left coordinate $y$" and "$x$ is an ordered pair with right coordinate $y$." Note that the expression "$u=\langle v,w\rangle$" is really shorthand for "$\pi_0(u,v)\wedge\pi_1(u,w)$."
Writing out the projection relations in terms of $\in$ alone is a good exercise. Once you've done this, you can produce $B$ by applying Separation to the formula
$$\varphi(x)\equiv \forall s,t(\pi_0(x,s)\wedge \pi_1(x,t)\rightarrow s<5\wedge t<4).$$
Separation applied to this formula, with "container set" $z=\mathbb{N}\times \mathbb{N}$, says that there is a set $B$ consisting of exactly those $a$ which are elements of $z$ and which satisfy $\varphi$ - and this $B$ is precisely what we want.
A: Here is a possible workaround in order to show that $B$ is a set:
You could use a single variable $w$ (to encode the pair $\langle s,t\rangle$) and then use
$$\phi(w):=\exists s\exists t\;\, w=\,\langle s,t\rangle \land s<5 \land t<4$$
A: You can choose $\varphi(x)$ to be $x_0<5\land x_1<4$, if you have the notation $x=\langle x_0,\,x_1\rangle$ for $2$-tuples. Mathematicians often abbreviate this by saying $\varphi(\langle s,\,t\rangle)$ iff $s<5\land t<4$, with it being taken as implicit that $\neg\varphi(x)$ whenever $x$ isn't a $2$-tuple (although that wouldn't matter in the present context).
However, the existence of a Cartesian product $X\times Y$, such as $\Bbb N\times\Bbb N$, is proven with several axioms:

*

*First we convince ourselves ordered pairs exist, e.g. on Kuratowski's definition with unordered-pair (an axiom in Zermelo set theory, a theorem in ZF) repeatedly.

*Replacement tells us first that $X\times\{a\}$ exists for each $a\in Y$, then that there is a set of these Cartesian products.

*We can now take a union to get $X\times Y$.

If this question presupposes we already accept the above, we can prove $B$ exists by writing $B=X\times Y$ with$$X=\{s\in\Bbb N|s<5\},\,Y=\{t\in\Bbb N|t<4\},$$which lets us use comprehension twice, with very obvious choices of $\varphi$.
