Meaning of the statement $\forall x \exists y \forall z (z \neq y \iff f(x) \neq z)$
The statement is  

"for all $x$, there exists a value of $y$ such that for all $z$,
$z\neq y$ if and only if $z \neq f(x)$".

This can be simplified:
$$\begin{align}
&amp; &amp; \forall x \exists y \forall z (z\neq y \iff z \neq f(x))\\
&amp;\implies &amp; \forall x \exists y \forall z (z=y \iff z = f(x))\\
&amp;\implies &amp; \forall x \exists y \forall z (y = f(x))\\
&amp;\implies &amp; \forall x \exists y (y = f(x))\\
\end{align}$$

If we denote the set of all values of $x$ by $X$ and the set of all values of $y$ by $Y$, then this tells us that the function $f$ maps every $x$ in $X$ to a $y$ in $Y$.  That is, $f: X \to Y$.