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?
No. If you have a function symbol, then it is implicit that any terms that you can produce with it exists and well-defined when you interpret the term.
Specifically, if $g$ is the symbol of your ordered pair operator, and $M$ is a structure to your language $\{\in,g\}$, then you require that $g$ is defined on $M^2$, so for every $x,y\in M$, $g(x,y)$ is some element of $M$, which in other words means that it exists.