Why do definitions need to be 'proved' to work? I am reading Elements of set theory by Enderton. I am having a conceptual difficulty with why it seems that certain definitions almost have to be 'proved' to work?
Specifically, I am reading about defining an ordered pair set such that $$\langle x,y \rangle = \langle u,v \rangle$$
are identical objects.
He describes how it is defined as:
$$\langle x,y \rangle = \{\{x\},\{x,y\}\} $$
and also describes various definitions that do not work, such as $$\langle u,v \rangle = \{x,y\}$$
What I don't understand is why either of these are necessary. In his final remark on the section he states 'The preceeding theorem lets us unambiguously define the first coordinate of $\langle x,y \rangle$ to be $x$, and the second coordinate to be $y$'. If this is the ultimate goal, why does it matter that we 'show' the definition works in this way? Why can't we simply say, 'Whenever something of the form $\langle x,y \rangle$ is used, it is an ordered pair and $x$ is the first coordinate and $y$ is the second coordinate.'?
I am only just learning more formal mathematics now, such as the axiomatic approach and so forth, so apologies if I am missing something obvious.
 A: We need to prove that something with the desired properties actually exists. For example, consider the statement:

We write "$\mathfrak{Q}$" to denote the set of all sets not containing themselves.

This "makes sense" linguistically, but hides a crucial assumption: that the set of all sets not containing themselves actually exists. And in fact it does not - this is the conclusion of Russell's paradox.
So we could talk "non-specifically" about some arbitrary ordered pairing notion, but we need to first prove that such a thing exists (and incidentally, even expressing "there is a pairing operation" precisely in the language of set theory is nontrivial, since this pairing operation isn't literally a function - its domain is too large). And the easiest way to show  that (in fact, the only way I know) is to build one.

It might be a good idea at this point to consider situations where we want a pairing operator with certain additional properties, where it's not at all clear that such a thing exists. The standard example of such a thing is a flat pairing function.
A: Definitions do not need proof. Constructions do, if they are to satisfy a requirement.
Definition: An ordered pair is an object $P(x,y)$ such that $P(x_1,y_1)=P(x_2,y_2)$ iff $x_1=x_2$ and $y_1=y_2$.
In principle, ordered pairs need not exist. But they do:
Theorem: $P(x,y)=\{\{x\},\{x,y\}\}$ is an ordered pair.
On the other hand, not all constructions work:
Theorem: $P(x,y)=\{x,y\}$ is not an ordered pair.
