What is the definition of function in ZF/ZFC?
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)). $$