Function definition by cases.
It is usual define for example the absolute value of Real number as
$$ \left|x\right| = \begin{cases} x & if & x> 0 \\ -x & if &x < 0 \\ 0 & if & x = 0\end{cases} $$
However ZFC does not has anything like cases nor ifs
How this kind of function definition by cases can be written in the formal ZFC set theory?
Only for give you a context:
A function $f\colon X\to Y$ is a subset of $X\times Y$ such that $(x,y_1)\in f$ and $(x,y_2)\in f$ implies $y_1=y_2$.
so to define a specific function $F$ for given sets $A$ and $B$ one can write:
$$F = \{(x,y)\in A\times B : y = U(x)\}$$ in this case $B\subseteq P(U(A))$
or if $A$ is the Real numbers
$F = \{(x,y)\in \Bbb{R\times R}: y = \sqrt{x^2}\}$ and this is the obvious answer to my example but my question is the general handle of cases in defining functions formally in ZFC, the Direchlet function is another example with a a less obvious solution (but it do has too).
Let us consider the absolute value, to begin with. In $\sf ZFC$ there are formulas which define the real numbers, their order, the number $0$ in the real numbers, and the addition of the real numbers.
(Note that indeed there are many different ways to interpret and represent the real numbers as sets, but they all have the same properties, so it doesn't matter. So we just fix one way of doing that.)
Then we can define what is $-x$, given a real number $x$. It is the unique real number $y$ such that $x+y=0$.
Now we can define using the formulas which define $0_\Bbb R$ and $<_\Bbb R$ (and I will omit the subscript $\Bbb R$ from here on end) the sets $\Bbb R^-=\{x\in\Bbb R\mid x<0\}$ and $\Bbb R^+=\{x\in\Bbb R\mid 0<x\}$.
Finally we can define the function $|x|$ as the union of three functions, $F_1=\{(x,x)\mid x\in\Bbb R^+\}$, $F_2=\{(x,y)\mid x\in\Bbb R^-\land y=-x\}$ and $\{(0,0)\}$. We can now verify that the three are functions, and that their domains are disjoint. Therefore their union is a function as well, and we can now prove that this union is a function whose domain is $\Bbb R$.
More generally, if we want to divide into cases, we use the complicated formulas which define the real numbers, and the things we want to use, and then we define the various cases. If we ensured that no $x$ satisfies two incompatible cases (i.e. two cases which result in a different value), then the union of these is the function we wanted.
You can try and sit down to write such formulas, or start with the formulas defining $\Bbb R$ and its basics (order, addition, etc.), then write explicit formulas for the absolute value:
$$\{(x,y)\mid \exists z(\varphi_0(z)\land ((x=z\land y=z)\lor(\varphi_{<_\Bbb R}(x,z)\land\varphi_{+}(x,y,z)=0)\lor(\varphi_{<_\Bbb R}(z,x)\land x=y)))\}$$
Doing so for more complicated functions is, well, more complicated. The point is that we know how to do that mechanically.