Definition of function application in ZF-like theories

Question

What is the definition of function application in material set theories like ZF?

I know how functions are represented using functional relations (optionally paired with the codomain).

I'm aware of the definition of function application in other formal theories such as Martin-löf theory, but there it is a a primitive notion, defined as one of the natural deduction rules. In ZF-like set theories the sets representing functions are a derived notion.

Say I had an arbitrary functional relation $f$ representing some function and a a value $x$ in the domain of $f$. How is the operation that takes $f$ and $x$ and gives me the set $f(x)$ defined using the axioms and rules of ZF+FOL?

Answer 1

If $f$ is a functional relation, then $f(x)$ is simply a shorthand for the unique $y$ such that $(x,y)\in f$. More formally, in the language of set theory, if $\varphi(y)$ is a formula with free variable $y$, then if we write $\varphi(f(x))$ that is really a shorthand for the formula $\exists y((x,y)\in f\wedge \varphi(y))$ (where $(x,y)\in f$ is itself a shorthand, whose exact meaning depends on how you have chosen to encode ordered pairs in set theory).

Answer 2

$f(x)$ is defined to be the unique $y$ such that $\langle x,y\rangle\in f$. (The assumptions that $f$ is a function and that $x$ is in its domain ensure that there is a unique such $y$.)