I need to define in ZFC the following things:
Please describe a more or less formal way to describe these things in ZFC.
On
The axiom of replacement!
For the domain of a relation $R$, for instance: to each element $p$ of $R$ we may, definably, associate its left coordinate $p_0$. Then, using replacement, we get the set of all left coordinates, i.e. the domain. (I'm assuming by "domain" you mean $\{x: \exists y ((x, y)\in R)\}.$)
Exercise: show that replacement is necessary. (Hint: $V_{\omega+\omega}$ is a model of every $ZFC$ axiom except replacement. . .)
There are many, many ways to encode ordered pairs into sets. But they all have one necessary key: you can "decode" the first element, and you can "decode" the second element.
In the standard Kuratowski way, $(x,y)=\{\{x\},\{x,y\}\}$, and then $x$ is the unique element which is in both sets that appear in $(x,y)$; and $y$ is either equal to $x$, or it is the unique element of $\bigcup(x,y)$ which is not $x$.
Given a fixed way of encoding ordered pairs into sets, let $\pi_1(z,x)$ be the formula which takes in $z$ as an ordered pair and $x$, and returns true if and only if $x$ is the left coordinate of $z$. And let $\pi_2(z,y)$ be the similar formula for decoding the right coordinate.
So, given a set of ordered pairs, $f$ in your case:
$\operatorname{dom}(f)=\{x\mid\exists z\in f\ \exists y(\pi_1(z,x)\land\pi_2(z,y))\}$ is a set using the replacement axiom for $\exists y(\pi_1(z,x)\land\pi_2(z,y))$
$\operatorname{rng}(f)=\{y\mid\exists z\in f\ \exists x(\pi_1(z,x)\land\pi_2(z,y))\}$, is a set for similar reasons.
$f[X]=\{y\in\operatorname{rng}(f)\mid\exists x\in X\ (x,y)\in f\}$ is a set due to separation.