Using axiom of replacement to form a function $f$ So I was (re)reading Kunen's set theory textbook, and in it there is a lemma (I.6.9) that illustrate using Axiom of replacement to define a function.
Assume that $\forall x \in A\ \exists!y\ \varphi(x,y)$ and assume replacement. Then there is a function $f$ with dom($f$) = $A$ such that for each $x \in A$, $f(x)$ is the unique $y$ that satisfy $\varphi(x,y)$
In his proof, he define a new formula $\psi(x,z) := \exists y\ [\varphi(x,y )\ \wedge\ z = (x,y)]$. He then use replacement to form $f$ as {$z:\exists x\in A\ \psi(x,z)$}
My question is how does replacement come into play here since I always 'read' replacement as saying 'image of a (definable) function is a set'. 
Any insights is deeply appreciated.

You are reading Replacement correctly. But there is a subtle point here: if the domain and image of a definable function exist (read: are sets), then the function is also a set.
Indeed, the importance of Replacement here is that the image is a set, so there is a set $B$ such that $f\subseteq A\times B$.
