Is the Axiom of Replacement necessary to construct any function in ZFC?

A while back, I read a source that I believe mentioned something along the lines of needing the Axiom of Replacement to define functions in ZFC Set Theory. I was convinced the entire time up to that point that to define a function $f \colon X \longrightarrow Y$, one mearly considers it as a subset of the product $X \times Y$, and thus only needs the Axiom of Powerset in order to define the Cartesian product, and the Axiom Schema of Comprehension to define subsets satisfying a particular predicate. However, the more that I think about it, the more I am confused in trying to define a function by a single predicate as a subset $f = \{(x, y) \in X \times Y \mid P(x, y)\}$, where $P(x,y)$ describes that each $x \in Y$ is associated to a $\textit{unique}$ $y \in Y$. So which is it? What is the Axiom of Replacement really needed for? Thanks in advance.

I'm not sure how you think replacement comes into play here.

Given sets $X$ and $Y$, we can as you say form the set $X\times Y$ without invoking replacement in any way. Now, for any formula $\varphi(x, y)$ we can form the set $$R_\varphi=\{\langle x, y\rangle\in X\times Y: \varphi(x, y)\}$$ as follows:

Before I do this, note that this is not as trivial as it may first appear: "$\varphi(x, y)$" is a formula of two variables, not a formula of a single (ordered pair) variable. This is why I've used the angle-brackets notation for ordered pairs.

Namely, let $\psi_\varphi(z)$ be the formula "there are $x\in X, y\in Y$ such that $z=\langle x, y\rangle$ and $\varphi(x, y)$." Then $$R_\varphi=\{z\in X\times Y: \psi_\varphi(z)\},$$ which exists by separation. If, now, $\varphi$ happens to have the property that for each $x\in X$ there is exactly one $y\in Y$ with $\varphi(x, y)$, the set $R_\varphi$ is in fact a function. So replacement plays no role here.

What replacement/collection is used for is building the range of a definable "function"/"relation." Namely, if we have a formula $\varphi(x, y)$ (the definable "function") and a set $X$ (the domain) such that for each $x\in X$ there is exactly one $y$ with $\varphi(x, y)$ (but note, we don't know where these $y$s "live"), then without replacement we can't generally conclude that the set $\{y: \exists x\in X(\varphi(x, y))\}$ exists, hence we can't argue that the class $$\{(x, y): x\in X, \varphi(x, y)\}$$ actually is a set, and hence a genuine function.

So for example, in set theory without replacement we can take $X=\omega$, $\varphi(x, y)\equiv$ "$y=V_x$;" then we can prove that for each $x\in X$ there is exactly one $y$ with $\varphi(x, y)$, but we can't even prove that $V_\omega$ exists!

• Forget about my previous answer. This is a much more appropriate view on the matter. (Nothing of what I've said is factually wrong but replacement, in my answer, comes in to show the existence of certain ranges of functions. If you already know that such a range exists, Noah's answer shows how to form a desired function from it.) – Stefan Mesken Nov 24 '17 at 20:03
• Wouldn't the argument also work with $\phi(x,y)\equiv y=\omega+x$? – Hagen von Eitzen Nov 24 '17 at 21:03
• @HagenvonEitzen Yes, but it's much easier to show that $V_{\omega+\omega}\models$ Z than it is to show that there's a model of Z not containing $V_\omega$, so I find the $V_\omega$-version a bit more surprising. – Noah Schweber Nov 24 '17 at 21:04