What's the meaning of the axiom schema of replacement? The axiom schema goes:

We have $∀y(∃x:(∀z(P(y,z)⟺(x=z))))$.
Then we state as an axiom $∀w(∃x:(∀y((y∈w)⟹(∀z:(P(y,z)⟹(z∈x))))))$.

I've seen it expressed in English as

For any function $f$ and subset $S$ of the domain of $f$, there is a set containing the image $f(S)$.

What is $f$? Is it the function defined by $P(y,z)$ as explained in this post, or is it the propositional function $P(y,z)$ itself? Are $x,z,y$ the same as in the first part? Why to state that $x$ exists in the second part of the axiom schema, if its existence was already presumed in the first part?
 A: $f$ does not occur in the formal version. In fact, it is the function defined by the propositional function $P(y,z)$. That is, $P$ gives us an instance of the Axiom Schema of Replacement only if the first condition about $P$ is met (is a theorem). In that case, our $f$ is just the function that maps $x$ to the unique $y$ for which $P(x,y)$ holds. In other words, $$\forall x\forall y(P(x,y)\leftrightarrow y=f(x)).$$
Are $x,z,y$ the same? Not really. The first can be interpreted as 

For all 'inputs' $y$ there exists a 'function value' $x$ such that any 'other value' $z$ meeting the criterion of being a function value of $y$ is the same as $x$. 

The "semantic roles" of $x,y,z$ in the second part are different: 

For all 'domains' $w$ there exists an 'image set' $x$ such that for all elements $y$ of the domain, the function value $z$ is in $x$.

More generally, there is no reason to expect bound variables in different statements to be "the same" in any sense. But you might as well prefer to replace $x,y,z$ with $a,b,c$ in one (and only one) of the two statements.
