Confusion with the definition of a "Set Function" in the context of ZFC Here is the definition of a set function, provided by http://web.mat.bham.ac.uk/R.W.Kaye/logic/infinity.html.
However, before getting to that, the author uses the following notation for ordered pairs: "$\langle x, y \rangle$"...using the Kuratowski definition of $\{\{x\},\{x,y\}\}.$ Also, (I believe) because this is all within the scope of ZFC, the author refers to $x$ and $y$, individually, as sets. 
At any rate, here is the penned definition of a set function:

"Defintion. A set function is a set $f$ such that every element of $f$ is $\langle x,y \rangle$ for some sets $x,y$ and $\forall x,y,z (\langle x,y \rangle \in f \land \langle x,z \rangle \in f \rightarrow \color{red}{{x =z}})$."

Firstly, I wanted to make sure that I am correctly identifying the antecedent of this implication...the antecedent is the entire statement: "$\langle x,y \rangle \in f \land \langle x,z \rangle \in f$" 
Correct? And the consequent is "$x=z$", yes?
Secondly, I want to hone in on what I highlighted in $\color{red}{\text{red}}$. Specifically, I have no idea what this means. Had it said $y=z$, I would have thought, "Oh, okay. It's saying that each element in the domain only has one corresponding output (i.e. a unique output)"...which is the definition of a function that I am familiar with. 
But this statement of "$x=z$" means nothing to me. Is this a typo?
Thank you! 
 A: Yes, that's a typo: it should be "$y=z$," not "$x=z$."

To make this hopefully more intuitively (if only for other readers), let me point out the key parallel:


*

*Thinking of functions as "single-output relations," the natural language definition of "function" is: "Whenever $aRb$ and $aRc$ we have $b=c$."

*The set-theoretic parallel is "Whenever $\langle a,b\rangle\in R$ and $\langle a,c\rangle\in R$ we have $b=c$."
Remember that a relation is just any set of ordered pairs at all, so they're much easier to think about initially. 


*

*Hopefully pre-empting a possible question, we view the domain of a relation as being determined after the fact: $dom(R)=\{x:\exists y(\langle x,y\rangle\in R)\}$. Alternatively, we could require relations to come with a declared domain, allow relations to be partial, and add "For all $x\in dom(f)$ there is some $y$ with $\langle x,y\rangle\in f$" to the definition of "function." This is similar to how in set theory functions don't come with explicit codomains.

