The axiom schema of replacement needs a function, defined by ${\forall}y({\exists}x:({\forall}z(P(y,z){\iff}(x=z))))$, where $f(y)=x$.
My question is: why isn't ${\exists}$ replaced by ${\exists}!$?
Shouldn't it be specifically stated that there needs to be only a single $x$, since it's a function.
On
The idea is that you are defining $f(y)$ to be the unique $x$ such that $P(y,x)$ is true. If it said simply ${\forall}y({\exists}x:P(y,x))$ then you would be right that it needs to say $\exists!$ instead of just $\exists$. But notice that it says not just that there is an $x$ such that $P(y,x)$ but that there is an $x$ such that $P(y,z)\Leftrightarrow z=x$ for all $z$. This means that $P(y,z)$ is true when $z=x$, but it also means that $P(y,z)$ is not true when $z\not=x$. That is, $z=x$ is the only value of $z$ such that $P(y,z)$ is true. This says exactly that the $x$ such that $P(y,x)$ is true is unique.
To put it another way, ${\exists}x:({\forall}z(P(y,z){\iff}(x=z)))$ is just a way of writing $\exists! x: P(y,x)$ without using the symbol $\exists!$ (which is usually not taken as one of the primitive logical symbols).
On
The full statement of the axiom schema is as follows: given $\varphi(x,y,u)$, $$\forall u(\forall x(\forall a(a\in x\rightarrow\exists y(\varphi(a,y,u)\land\forall z(\varphi(a,z,u)\rightarrow y=z)))\rightarrow\exists w(\forall y(y\in w\leftrightarrow\exists a(a\in x\land\varphi(a,y,u)))))$$
Namely, if $\varphi$ is a formula which defines a function on $x$, then the range of that function, applied to $x$, is a set.
We already assume that for every $a\in x$ there exists a unique $y$ such that $\varphi(a,y)$ (and the fixed parameters).
No. The axiom already implies that there's only one such $x$.
Given $y$, let $x$ and $x'$ be elements with ${\forall}z(P(y,z){\iff}(x=z))$ and ${\forall}z(P(y,z){\iff}(x'=z))$. Using $z=x$ in the first statement yields $P(y,x)\iff(x=x)$, and thus $P(y,x)$; then using $z=x$ in the second statement yields $P(y,x)\iff(x'=x)$, and thus $x'=x$.