Is ZFC under two different encodings of ordered pairs equivalent? Let $\mathbf{ZFC}$ denote the theory of ZFC.
Let $\mathbf{ZF-R}$ denote the theory of ZF without replacement. The motivation is that the remaining axioms do not require ordered pairs.

Let $p(x,y,z)$ be a valid encoding for ordered pairs, where $p$ is a formula over the language of ZFC with $x,y,z$ being the only free variables, iff:
$$\mathbf{ZF-R} \vdash \forall x \forall y \exists! z [p(x,y,z)] \land \forall a \forall b \forall c \forall d \forall z [p(a,b,z)=p(c,d,z) \to a=c \land b=d]$$

Let $\mathbf{ZFC}^p$ denote ZFC under the encoding $p$.
If $a$ and $b$ are different valid encodings, do we necessarily have the property that for every sentence $\varphi$ over the language of ZFC (with signature $\{\in\}$), that $(\mathbf{ZFC}^a \vdash \varphi) \iff (\mathbf{ZFC}^b \vdash \varphi)$?
 A: As Eric mentioned, the Axiom of Replacement does not involve encoding. Let's talk about it for a minute, and let's omit all the parameters for simplicity.
Replacement states that given $\varphi(x,y)$, if $A$ is a set such that $\varphi$ is functional on $A$—namely, for every $a\in A$ there is exactly one $b$ such that $\varphi(a,b)$ holds—then $\{b\mid\exists a\in A:\varphi(a,b)\}$ is a set.
There are no ordered pairs involved here, since the functionality of $\varphi$ is given in the meta-level. Moreover, if you want to think about it in terms of functions as sets of ordered pairs, well, if a function exists, then its domain and range exist (granted you're using some reasonable definition of ordered pairs that lets you decode the left and  right coordinates in a uniform way).
So your question is more or less vacuous, since $\sf ZFC$ is the same regardless to your coding mechanism of ordered pairs. But here's something interesting to consider.

Theorem. The following are equivalent over $\sf ZF-R$:
  
  
*
  
*The Axiom Schema of Replacement.
  
*For every $\varphi(x,y,z,p)$, if given a fixed parameter $p$, $\varphi(x,y,z,p)$ can code "$z$ is the ordered pair $(x,y)$", then $\varphi$ and $p$ define a Cartesian product. In other words, for all $A$ and $B$, the following is a set: $$A\times_\varphi^pB=\{z\mid\exists a\in A\,\exists b\in B:\varphi(a,b,z,p)\}.$$
  

So the fact that we can use any schema to code our ordered pairs is itself equivalent to Replacement.

Now, let me answer what I think is your real question here. We seem to rely on the Kuratowski definition of ordered pairs very heavily in all the definitions. And maybe there's a better one that will let us "prove more" or whatever? But the fact is that set theory is not interested in what are ordered pairs, just like it is not really interested in what are the real numbers. 
When you prove, for example, that every bounded complex analytic function defined on the whole plane is constant, you are not proving this for a particular implementation of the complex numbers in $\sf ZFC$. Heck, the proof doesn't even mention sets.
If you look at this from a set-theoretic point of view, you have a naive proof that works because of certain properties (topological, algebraic, etc.), and what $\sf ZFC$ proves is that no matter how you choose to implement the notions involved (what is a function, what set is the complex numbers, etc.), if those implementation have the "expected properties", then the proof will work.
In that sense, what you actually from a foundational point of view, is a "template theorem". It is agnostic to how you code functions, or the complex numbers, or anything. As long as you give it an implementation that "works", it's going to be fine.

Let me remark something about the Axiom of Choice here. Choice seems as though it is particularly susceptible to our choice of ordered pairs. But this is not true for two reasons:


*

*We can always use the formulation: Every family of non-empty and pairwise disjoint sets has a transversal (a set which meets each of the members of the family on exactly one point); and more importantly

*Since the equivalence of Replacement mentioned above is not using Choice, once you have Replacement, you can freely move between any definition of function or well-order (both of which heavily depend on the implementation of ordered pairs). So again the choice of formulation does not matter.
A: To complement Asaf's answer, here is one way to say that all pairing notions are equivalent:
Let's say that a pairing notion is a formula $\pi(x, y, z)$ such that ZFC proves each of the following:


*

*ZFC proves that for all $x, y$ there is exactly one $z$ such that $\pi(x, y, z)$ holds.

*ZFC proves that for all $x_0, y_0, x_1, y_1, z$ we have $$\pi(x_0, y_0, z)\mbox{ and }\pi(x_1, y_1, z) \iff x_0=x_1\mbox{ and }y_0=y_1.$$
Then suppose $\varphi, \psi$ are two different pairing notions. The two crucial results, to my mind, are:
First, the ability to convert between pairing notions:

The "conversion operation" - the class function which sends $z_0$ to $z_1$ iff $\varphi(x, y, z_0)$ and $\psi(x, y, z_0)$ both hold for some $x, y$ - is definable in the obvious way (and ZFC proves that the definition works properly).

And second, the existence of Cartesian products:

For each formula $\pi$ in the language of set theory, ZFC proves that if $\pi$ is a pairing notion then for all sets $X$ and $Y$ the set $\{z: \exists x\in X, y\in Y(\pi(x, y, z))\}$ exists.

(This is just the parameter-free version of fact (2) in the theorem in Asaf's answer; note that adding parameters doesn't change the situation in any way.) These two facts demonstrate that what pairing notion we use really makes no difference (at least, within ZFC - for weaker set theories things get more complicated, and the choice of pairing function may be important).
