Q:

What is the definition of function in ZF/ZFC?

In ZF there is axiom schema of replacement, which can be stated as

the image of a set under any definable function will also fall inside a
  set

Is there a definition of the concept of function in ZF/ZFC? What is it? I mean set-theoretically speaking. That is, in naïve set theory function can be understood as a set of pairs (triples, etc.), but what about ZF/ZFC?

A:

There are two different notions which are both called "function". A function internally to ZFC is a set of pairs, where the first element of the pair is understood to be mapped to the second by the function. For example, the successor function $S :\mathbb N \to \mathbb N$ is a function internally in ZFC, and it is given by
$$
S = \{(n,m) \in \mathbb N \times \mathbb N \mid m = n + 1\}.
$$
However, the function from the axiom schema of replacement refers to a function on the universe given by a formula. Slightly simplified, if $\phi(x,y)$ is a formula with two free variables such that ZFC proves that $\forall x \exists y \phi(x,y)$ and $\forall x \forall y \forall y'(\phi(x,y) \land \phi(x,y') \to y = y')$, then there is an instance of the schema axiom of replacement which states
$$
\forall X \exists Y(\forall x\forall y(\phi(x,y) \land x \in X \to y \in Y)).
$$

