If $X$ and $Y$ are sets, their cartesian product $X\times Y$ is a set. In ZFC set theory, every element object is a set. We know or feel that if $X$ and $Y$ are sets, their cartesian product $X\times Y$ is a set.
My question is: Why if $X$ and $Y$ are sets, their cartesian product $X\times Y$ is a set?
 A: tldr; $X\times Y$ is a definable subset of $\mathcal{P}(\mathcal{P}(X \cup Y))$ (assuming that you're using, say, the Kuratowski definition of an ordered pair).
More precisely, suppose $(x,y) = \{\{x\},\{x,y\}\}$.  Given the elements $x \in X, y \in Y$, the sets $\{x\}$ and $\{x,y\}$ are in $\mathcal{P}(X \cup Y)$, so the set $\{\{x\},\{x,y\}\} \in \mathcal{P}(\mathcal{P}(X \cup Y))$.  Then define $X\times Y$ to be the set of all sets $z$ in $\mathcal{P}(\mathcal{P}(X \cup Y))$ such that there are $x,y$ with $z=(x,y)$. You need to do a little bit more than this to actually create a wff in the first-order language of set theory, but not that much more.
For a full wff, we have the following:
$$\varphi(z) = \exists x\exists y\exists v\exists w(x\in X \wedge y\in Y \wedge \mathrm{pair}(v,x,x) \wedge \mathrm{pair}(w,x,y) \wedge \mathrm{pair}(z,v,w))$$
where
$$\mathrm{pair}(z,x,y) = \forall w (w\in z \leftrightarrow ((w=x)\vee (w=y))$$
In other words, $\mathrm{pair}$ is a wff with three free variables which expresses the fact that $z=\{x,y\}$. $\varphi$ expresses that $z$ is itself a pair of elements $v,w$ which are respectively, $v=\{x,x\}=\{x\}$ and $w=\{x,y\}$.  In other words, $z=\{\{x\},\{x,y\}\}$.
Then
$$X\times Y = \{ z \in \mathcal{P}(\mathcal{P}(X\cup Y) \mid \varphi(z)\}$$
(note that $\varphi$ has the parameters $X,Y$).
This uses the Axiom of Power Set, Axiom of Pairing, Axiom of Union,  and the Axiom Schema of Restricted Comprehension.
Why didn't we just say
$$X\times Y = \{ (x,y) \in \mathcal{P}(\mathcal{P}(X\cup Y)) \mid x\in X \wedge y\in Y\}$$
?
Well, recall what the Axiom Schema of Restricted Comprehension actually says: for every set $X$ and every wff $\varphi(x)$ with the free variable $x$, there exists a set $Y$ whose elements are exactly those in $x\in X$ which satisfy $\varphi(x)$. But the aforementioned 'definition' isn't in that form!
How do we normally get away with this, though? Certainly we say things like $\{f(x)\in Y \mid x\in X\}$ for the image of a function $f$! This uses another axiom of $\mathsf{ZFC}$, called the Axiom Schema of Replacement.  As shown above, we don't need to use it, and judging from the answer you had written up, it seems you haven't gotten to Replacement yet.
A: Proof. Since $x\in X$, we have $x\in X\cup Y$. Similarly, $y\in X\cap Y$.It follows that the sets {$x$} and {$x,y$} are subsets of $X\cup Y$ and hence elements of $\mathcal{P}(X\cup Y)$. Therefore, {{$x$},{$x,y$}} is a subset of  $\mathcal{P}(X\cup Y)$. Hence, $(x,y)=${{$x$},{$x,y$}}$\in  \mathcal{P}(\mathcal{P}(X\cup Y))$ . Thus all the elements of $X\times Y$ are elements of $\mathcal{P}(\mathcal{P}(X\cup Y))$. Now among the elements of $\mathcal{P}(\mathcal{P}(X\cup Y))$ we will distinguish the ones of the form $(x,y)$ by a formula $\mathcal{P} (z)$, i.e., by a property. In other words, we will find a formula $\mathcal{P} (z)$ such that for all $z$, the following will hold:
$\mathcal{P} (z) \Leftrightarrow \exists x\exists y(x\in X\wedge y\in Y\wedge z=${{$x$},{$x,y$}$)$.
If we can do this, then we will have $X\times Y=$ {$z\in\mathcal{P}(\mathcal{P}(X\cup Y)):\mathcal{P}(z)$}, and so by A3, $X\times Y$ will be a set. 
