A proof in naive set theory. I am trying to use naive set theory to figure out a proof of the following statement:
$$(x = u \land y = v) \to 〈x, y〉 = 〈u, v〉$$.
What propositions should i use to prove this?
 A: The logic of the identity relation tells you that, if $T$ is any theory with a standard identity predicate, and $f(\cdot)$ is a one-place functional expression constructible in $T$, then
$$x = u \vdash_T f(x) = f(u).$$
That's just immediate from one of the basic rules governing identity. (If you don't know that, you need to check out the rules for identity in a standard textbook.)
Two applications of that same rule will tell you that if $g(\cdot, \cdot)$ is any two-place functional expression, then, equally trivially
$$x = u, y = v \vdash_T  g(x, y) = g(u, v).$$
which of course immediately implies (assuming $T$ has a sensible logic!)
$$\vdash_T  (x = u \land  y = v) \to  g(x, y) = g(u, v).$$
So to get your desired conditional, all you need to know about the construction $\langle \cdot, \cdot\rangle$ is that is a two-place functional expression of the theory $T$. In the particular case where $T$ is a set theory, naive or fancy, then  $\langle \cdot, \cdot\rangle$ is of course such a functional expression: the function $x, y\mapsto \langle x, y\rangle$ maps $x$ and $y$ to [some set which will serve as] their ordered pair, whatever exactly that might be -- which doesn't matter. So there you go, your conditional 
$$\vdash_T  (x = u \land  y = v) \to  \langle x, y\rangle = \langle u, v\rangle.$$
follows trivially from the logic of identity.
The fun non-trivial direction (given a specific definition for $\langle \cdot, \cdot\rangle$) is to show the converse conditional: 
$$\vdash_T  \langle x, y\rangle = \langle u, v\rangle \to  (x = u \land  y = v),$$
and thereby confirm that your favoured version of $\langle \cdot, \cdot\rangle$ indeed delivers an implementation of ordered pairs. But that isn't what you asked!
