How to rigorously prove from set theory that functions can be composed? This is a follow up to my previous question about existence and uniqueness of piecewise functions. Suppose we are given two functions $f:S \rightarrow T$ and $g:T \rightarrow U$. How does one prove from ZFC set theory that there is a unique function $h:S \rightarrow U$ which is the composition of those two functions?
 A: I'm using the definition $A \to B = \{f \in P(A \times B) | \forall x \in A \exists ! y \in B (x, y) \in f\}$. That is, a function is a set of input-output pairs such that every input corresponds to a unique output.
Define $h = \{(x, y) \in S \times U | \exists z \in T ((x, z) \in f \land (z, y) \in g)\}$. I claim that $h$ forms a function $h : S \to U$.
First, we must prove that $h$ is a set at all. But we know that $h$ is a set because $S \times U$ is a set (by other axioms) and we can pick $h$ out as a subset of $U$ using the axiom schema of separation.
Now, we must prove that $h$ is a function (proving uniqueness). Suppose we have $(x, y) \in h$ and $(x, y') \in h$. Then take $z \in T$ such that $(x, z) \in f$ and $(z, y) \in g$. And take $z' \in T$ such that $(x, z') \in f$ and $(z', y') \in g$. Then since $f$ is a function, $z = z'$. So we see that $(z, y) \in g$ and $(z, y') \in g$. Then since $g$ is a function, we have $y = y'$.
Now, we prove that $h \subseteq S \times U$. Suppose we have $(x, y) \in h$. Then take $z \in T$ such that $(x, z) \in f$ and $(z, y) \in g$. Since $f \subseteq S \times T$, we see that $x \in S$. And since $g \subseteq T \times U$, we see that $y \in U$. Then $(x, y) \in S \times U$.
Finally, we prove existence. Suppose we have $x \in S$. Then take some $z \in T$ such that $(x, z) \in f$. Then take some $y \in U$ such that $(z, y) \in g$. Then $(x, y) \in h$.
Thus, we see that $h : S \to U$.
Note that we do not ever need the axiom schema of replacement, the axiom of foundation, or the axiom of choice in proving this theorem.
