Can a notation for ordered pairs in ZFC set theory be introduced as a conservative extension of ZFC without junk theorems? Currently, a standard way to introduce ordered pairs in ZFC set theory is to define
an ordered pair $(a,b)$ as $\{\{a\},\{a,b\}\}$. From this definition one can deduce the main property of ordered pairs:
$(a,b) = (x,y) \rightarrow a=x \,\&\, b=y$.
But some junk theorems can also be proved, for example, $(a,a) = \{\{a\}\}, \{a\} \in (a,b)$, etc.
see also https://mathoverflow.net/questions/90820/set-theories-without-junk-theorems
https://mathoverflow.net/questions/386756/a-better-way-to-introduce-ordered-pairs-in-zf
For a different approach see the paper "Adding an Abstraction Barrier to ZF Set Theory"
https://link.springer.com/content/pdf/10.1007%2F978-3-030-53518-6_6.pdf
An excerpt from it:
" Such ‘accidental theorems’ do not match how people think about the mathematics and also cause practical difficulties when using set theory in machine-assisted theorem proving."
So a natural question arises: is it possible to introduce ordered pairs in a more safe way, without possibility to get
such strange "theorems".
A rather natural approach is to extend ZFC just by adding a new function symbol (say $\pi$, it is usually omitted)
and a defining axiom such as  $\pi(a,b) = \pi(x,y) \rightarrow a=x \,\&\, b=y$
and prove that such theory extension is conservative (without such proof we can get an undesirable result, in a worse case - an inconsistent theory).
So my question:
Is this extension of ZFC (by adding the function symbol $\pi$ and its defining axiom)  conservative?
 A: Yes, in the strongest possible sense: if $M\models\mathsf{ZFC}$ then $M$ has an expansion to a model $M'$ of the theory you describe (that is, there is an $M'$ satisfying your theory whose reduct to $\{\in\}$ is exactly $M$ itself). Specifically, any of the usual set-theoretic implementations of ordered pairs can be taken to be $\pi^{M'}$.

*

*EDIT: in response to a comment below, let me explain in detail why this fact about extensions implies conservativity. Suppose your theory were to prove some sentence $\varphi$ purely in the language of set theory (i.e. no reference to $\pi$). I claim $\mathsf{ZFC}$ must already prove that sentence. For otherwise take some $M\models\mathsf{ZFC}+\neg\varphi$. By the previous paragraph it has some expansion $M'$ satisfying your theory. But since your theory entails $\varphi$ this means $M'\models \varphi$. But $M$ is the reduct of $M'$ to the language of pure set theory, so we get $M\models\varphi$ as well, a contradiction.

This may feel silly but it's not: we avoid junk theorems about $\pi$ even if we consider such expansions because of the different ways ordered pairs can be implemented in set theory. E.g. considering the difference between the Kuratowski ordered pair $\langle a,b\rangle_{K}=\{\{a\},\{a,b\}\}$ and the Hausdorff ordered pair $\langle a,b\rangle_H=\{\{a,1\},\{b,2\}\}$ we have that neither $\forall x(\{x\}\in\pi(x,x))$ nor $\exists x(\{x\}\not\in\pi(x,x))$ is a theorem of the new system.
A: Whatever we want of ordered pairs is absolutely not only the famous implication. I believe that (a,b) being Goedel-constructible in a,b is a sine qua non in set theoretic practice above 5 or so introductory lectures, and so is (a,b) being easily coded by a real provided a,b are reals, and zillion more such properties. So an abstract non-definable Bourbaki-style pair in the language will not work.
A: It is indeed conservative. We can prove that it is conservative quite simply. In fact, it's easy to show that $ZFC + \pi + Q$ is conservative, where $Q$ is the axiom $\forall a \forall b (a, b) = \pi(a, b)$.
This follows from a general result in logic which states the following: consider a theory $T$ and a statement $P$, where $FV(P) \subseteq \{x_1, x_2, ..., x_n, y\}$. Suppose that $T \vdash \forall x_1 \forall x_2 ... \forall x_n \exists ! y P$. Then consider the new theory $T$, which is $T$ with added $n$-ary function symbol $f$ and axiom $\forall x_1 \forall x_2 ... \forall x_n P[y \mapsto f(x_1, x_2, ..., x_n)]$, where $[y \mapsto f(x_1, x_2, ..., x_n)]$ is capture-avoiding substitution. Then $T'$ is a conservative extension of $T$.
Therefore, $ZFC + \pi$ is conservative.
