Am I allowed to realize one object twice within one set-theory? Say I consider a set theory with the Axioms of Extensionality and the Axiom of Pairing.
As I understand it, stating the axiom allows me to make a definition like
$$(a,b):=\{\{a\},\{a,b\}\}$$
and work with that $(a,b)$ in the context of my theory. Pairing says "it exists" (I can write it down with my language) and Extensionality says the abstract idea of it is unique as a set.

Is that way of thinking correct? Is that the purpose?

Because (if I know $a$ and $b$ exists and since I know what set brackets are) in a way I feel the set $\{\{a\},\{a,b\}\}$ existed already before the existence of a pair was guaranteed by the axiom - the possibility of nesting of sets as for the definition seems to be apriori to me, I asked a related question here.
Secondly, since there are more set-constructions of the ordered pair, like say
$$(a,b)':=\{b,\{a,b\}\}$$
as an alternative, I wonder:

Am I allowed to realize the ordered pair twice in one theory?

Then I could for example put ordered pairs as elements of ordered pairs of the second type and so on.

Is there really only one realization of the ordered pair in say ZFC or are there in fact all thinkable versions in the theory and we just choose one if we prove stuff about the abstract thing (which implies that the statements are true for all models)?

Or another idea: Should I view the whole thing in a way that I only define the thing using a concrete relization so that I can prove stuff about the "actual" abstract object, which is really only implicitly postulated to exist in the axiom. 
If that point of view ist true then I don't really see what the real difference of two realizations can be. 
 A: I think I wrote this as an answer to one of your previous questions and then I deleted it (I think Henning wrote another answer incorporating the point I was making).
We hardly make actual use of the properties of an ordered pair beyond the fact that it is actually a collection of two elements which may not be distinct and the order does matter.
Much like the proofs in real analysis do not depend on how you interpret the real numbers within a model of ZFC, but rather on the properties of the structure, a similar thing can be said here.
What we write when we write a proof is more of a schema for a proof. We consider abstract (non-pure set) objects and we say "plug the definition here, and insert the definition there". Ordered pairs make an excellent example as they appear almost everywhere. However there are only a few places where you actually care for the contents of the interpretation of the ordered pair.
Most of the time you care about the fact that an ordered pair allows you to distinguish between the two elements, even if they are the same (e.g. $\langle a,a\rangle$). As long as you have a way of telling which is the left coordinate and which is the right there is no real danger in replacing the definition.
However you should remember, again, that every time you are using an instance of the replacement axiom schema in contexts of ordered pairs then the axiom you are using may be different; but the logic behind the proof remains the same.
A: You can realize ordered pair as many ways as you want, but what's the point? What matters is not how you implement the ordered pair but the fundamental property that an ordered pair ought to satisfy, namely that $(a, b) = (a', b')$ if and only if $a = a'$ and $b = b'$. 
