If one wishes to introduce ordered pairs to ZFC as a new sort, rather than constructing them as sets (e.g., using the Kuratowski pairing function) within ZFC, it is possible to add a binary function symbol, e.g., "$g$", which given any pair of objects, returns an object of type "ordered pair."
One then includes the axiom that the output of $g$ satisfies the characteristic property of the ordered pair, i.e., that for all objects $a_1$, $a_2$, $b_1$, and $b_2$, $g(a_1,a_2) = g(b_1, b_2)$ if and only if $a_1 = a_2$ and $b_1 = b_2$.
However, is it also necessary to include as an axiom that ordered pairs exist? Terence Tao writes on page 62 of Analysis I, where he defines ordered pairs,
Strictly speaking, this definition is partly an axiom, because we have simply postulated that given any two objects $x$ and $y$, that an object of the form $(x, y)$ exists.
Similarly, Robert Wolf writes as the fourth of the "Set axioms" listed in Appendix 1, A General-Purpose Axiom System for Mathematics, on page 372 of Proof, Logic, and Conjecture / The Mathematician's Toolbox,
For every $x$ and $y$, the ordered pair $(x,y)$ exists.
But isn't that $g(a,b)$ exists for all objects $a$ and $b$ implicit in the fact that $g$ is defined as a binary function symbol? For example, in Peano arithmetic, with the unary successor function symbol $S$, I don't think it's necessary to explicitly axiomatize that $S(n)$ exists for all natural numbers $n$--isn't this implicit in the fact that $S$ is a unary function symbol?