Using axiom of replacement to form a function $f$

Question

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.

Answer 1

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$.

Answer 2

In Kunen [1] the axiom schemas Comprehension and Replacement are separate. Replacement says that if no variables occur free in $\varphi$ except possibly $x,y$ and if $\forall x\in A\,\exists! y\,(\varphi (x,y))$ then $$\exists B\,\forall y \,([\exists x\in A\,\varphi (x,y)]\implies y\in B).$$ Comprehension then says that $\exists C \,\forall y\,(y\in C\iff [y\in B\land \psi (y,A)])$ where $\psi (y,A)$ is $\exists x\in A\,( \varphi (x,y)).$ That is, there exists $C$ such that $$C=\{y:\exists x\in A\,(\,\varphi(x,y)\,)\}.$$ In Set Theory a function $is$ its graph. To get from $\forall x\in A\,\exists! y\,(\varphi(x,y))$ to $\exists f\,\forall z\,(z\in f\iff \exists (x,y)\,[x\in A\land \varphi (x,y)\land z=(x,y)])$ requires some more applications of R & C.

On the other hand, if the function $f$ exists with dom($f)=A$ then the above use of R& C does show that $\{f(x):x\in A\}$ exists.

Comprehension say that if $B$ exists then so does the collection of all, and only, the members of $B$ with some stated property $\psi$. Replacement says that if $\varphi$ intuitively "should" define a function on $A$ then all the members of the image of this alleged function belong to some set $B$, and then Comprehension can "extract" $C$, the image of $A,$ as a subset of $B$.

[1]. Kunen,K. Set Theory: An Introduction To Independence Proofs. 1st edition.