What ZFC axiom guarantees the existence of a domain set and a range set?

Question

Suppose we are working with the Kuratowski definition of ordered pairs, and that a relation is a set of ordered pairs. What axiom guarantees that $\operatorname{dom}(R) = \{ x : \exists y \langle x, y \rangle \in R\}$ and $\operatorname{ran}(R) = \{y : \exists x \langle x, y \rangle \in R\}$ are sets? I think that the axiom of replacement should be enough, but I am not so sure.

Answer 1

Instead of replacement, you could use the axioms of union and of separation (unless of course you treat separation as a consequence of replacement rather than an axiom). With Kuratowski's definition of ordered pairs, if $R$ is a relation then $\bigcup\bigcup R$ is the union of the domain and range of $R$,from which you can extract the domain and the range by separation.

The reason for pointing out this alternative approach is that it works even in Zermelo set theory, which is weaker than Zermelo-Fraenkel set theory.

Answer 2

You're right that that'll work (though as another answer mentions, it's not the only usable approach). Given a relation $R$, replacement maps any $(x,\,y)\in R$ to $x$, giving the domain. The range follows similarly. All you need is a definition of ordered pairs that implies their coordinates are uniquely defined.