How to encode the "statement to be proven" for the existence of the cartesian product in FOL. One of the exercises I am trying to carry out is proving the existence of the cartesian product $S \times T$ for any two arbitrary sets $S$ and $T$. My question is not about how to construct this set (I feel fairly good-to-go with that).
I am trying to develop my ability to document what exactly it is that I am proving. I have two questions about the First Order Logic syntax of the overall statement I am trying to prove.

Firstly: is the overarching statement effectively something along the lines of: $$\forall S,T \  \exists \ N \varphi(N)$$ where $N$ is the "$S \times T$" and $\varphi(N)$ refers to the properties we associate with a cartesian product?
Secondly: when I am trying to demonstrate that this can be done for any arbitrary sets $x$ and $y$ (which would then generalize to any two sets), it seems like I am trying to prove an implication that looks something like (written in pseudo-FOL / English):
$$ x \ \text{and}\  y \ \text{are sets that can be constructed in our domain of discourse} \rightarrow x \times y \  \text{is a set that can be constructed in...etc }$$
I am a little uncertain about my proposed answer to the second question because I am unsure of how to encode the property "can be constructed in our domain of discourse" using FOL.
I've previously seen the following syntax to establish that "something exists": $\exists x (x=x)$.
So maybe the implication is better written as:
$$\exists x (x=x) \land \exists y (y=y) \rightarrow \exists x \times y ( x \times y = x \times y)$$

You can probably see that this question generalizes to the construction of any sets (not just the particular instance of the cartesian product set), so please feel free to speak more generally.
Looking forward to the input!
Thanks~

Edit:
Using the proper syntax provided by Mauro Allegranza below...
We set out to prove the following statement:

$\forall S \forall T \exists C \forall z [z \in C \leftrightarrow z \in \mathcal P( \mathcal P (S \cup T)) \land \exists x \exists y (x \in S \land y \in T \land z=(x,y))].$

Now, the way I would approach this is the following:

Consider two arbitrary sets $N$ and $M$.
Prove the following:
$\exists C \forall z [z \in C \leftrightarrow z \in \mathcal P( \mathcal P (N \cup M)) \land \exists x \exists y (x \in N \land y \in M \land z=(x,y))]$
If I can prove the above statement for arbitrary sets $N$ and $M$, then I have proven it for any two sets.

My question is...what am I "doing" (in the context of FOL) when I assert - "Consider two arbitrary sets $N$ and $M$." What is this statement? Does it have a truth value / interpretation? Is it an "English abbreviation" for some sort of FOL syntax?
 A: We have that: $S \times T = \{ (x,y) \mid x \in S \text {  and  } y \in T \}$.
Thus, a suitable formula defining it would be: $\exists C \forall z [z \in C \leftrightarrow \exists x \exists y (x \in S \land y \in T \land z=(x,y))]$.
But this is not enough, because in order to asserts that set $C$ exists we have to apply Separation.
In order to do this, we have to find a suitable set $A$ from which "separate" it.
If we adopt the common Kuratowski's encoding of $(x,y)$ as $\{ \{ x \}, \{ x,y \} \}$ we have, for $x \in S$ and $y \in T$, that:

$\{ x \} \in \mathcal P(S)$ and $\{ x,y \} \in \mathcal P (S \cup T)$.

Thus, $(x,y) \in \mathcal P( \mathcal P (S \cup T))$.
In conclusion, the correct instance of the axiom will be:

$\forall S \forall T \exists C \forall z [z \in C \leftrightarrow z \in \mathcal P( \mathcal P (S \cup T)) \land \exists x \exists y (x \in S \land y \in T \land z=(x,y))].$

The formula says that, for every pair of sets $S$ and $T$ their cartesian product $S \times T$ exists.
