Unique existence and the axiom of choice The axiom of choice states that arbitrary products of nonempty sets are nonempty. 
Clearly, we only need the axiom of choice to show the non-emptiness of the product if 
there are infinitely many choice functions. If we use a choice function to construct a mathematical object, the object will often depend on the specific choice function being used. So constructions that require the axiom of choice often do not provide the existence of a unique object with certain properties. In some cases they do, however. The existence of a cardinal number for every set (ordinal that can be mapped bijectively onto the set) is such an example.

What are natural examples outside of
  set theory where the existence of a
  unique mathematical object with
  certain properties can only be proven
  with the axiom of choice and where the
  uniqueness itself can be proven in ZFC (I
  don't want the uniqueness to depend on
  a specific model of ZFC)? 

The next question is a bit more vague, but I would be interested in some kind of birds-eye view on the issue.

Are there some general guidelines to understand in which cases the axiom of choice can be  used to construct a provably unique object with certain properties?

This question is motivated by a discussion of uniqueness-properties of certain measure theoretic constructions in mathematical economics that make heavy use of non-standard analysis. 
Edit: Examples so far can be classified in three categories: 
Cardinal Invariants: One uses the axiom of choice to construct a representation by some ordinal. Since ordinals are canonically well ordered, this gives us a unique, definable object with the wanted properties. Example: One takes the dimension (as a cardianl) of a vector space and constructs the vector space as functions on finite subsets of the cardinal (François G. Dorais).
AC Properties: One constructs the object canonically "by hand" and then uses the axiom of choice to show that it has a certain property. Trivial example:  $2^\mathbb{R}$ as the family of well-orderable sets of reals.
Employing all choice functions: Here one gets uniqueness by requiring the object to contain in some sense all objects of a certain kind that can be obtained by AC. Examples: The Stone-Čech compactification as the set of all ultrafilters on it (Juris Steprans), or the dual space of a vector space, the space of all linear functionals. (Martin Brandenburg) The AC is used to show that these spaces are rich enough. Formally, these examples might be categorized in the second category, but they seem to have a different flavor.
 A: If you are satisified with your example of the cardinals as unique objects defined using choice then there is an easy answer to your question. Note that there is not a unique ordinal which is in bijective correspondence with each set; there are many, but there is always a least one which we call a cardinal. So the uniqueness comes from the well ordering of the ordinals. Given the axiom of choice you can always well order the domain of objects in which you are interested and then choose the least one. This will of course, be unique, but I doubt this is what you had in mind. But I think it does show that a better example than the cardinals is needed for uniqueness.
One can construct saturated models by transfinite induction and then show that, under certain circumstances, these are unique. One also has $\beta \mathbb{N}\setminus \mathbb{N}$ which needs choice to be non-empty, and it is also unique --- but probably also not what you had in mind.
A: In A definable nonstandard model of the reals, Kanovei and Shelah surprisingly managed to prove the existence of a ZFC-definable (i.e., specifiable via an explicit ZFC construction) nonstandard model of the reals. The existence of a nonstandard model of the reals is known to require a version of AC.
A: When you say "unique," how strictly do you mean it?  For instance, would you be happy to see examples of algebraic objects that are shown to exist with the axiom of choice, and are unique up to isomorphism?
A possible example that comes to mind is the construction of the injective hull of a module $M$ over a ring.  The argument that I know to embed a module into an injective requires Baer's criterion, which seems to require the axiom of choice.  After embedding $M$ into an injective, one must then cut down to a minimal injective submodule containing $M$, and this also seems to use choice.
However, if an injective hull exists then it seems to me that it's unique up to isomorphism without requiring the axiom of choice.
(Notice, this is one case where the object is unique up to isomorphism, but not unique up to unique isomorphism.  A similar example is the algebraic closure of a field $K$.  I almost quoted this as an example of the phenomenon above, but I realized that the proof of the uniqueness of $\overline{K}$ in Lang's Algebra, for instance, uses choice.)
A: I use the following — hopefully correct — interpretation of the question: We look for examples where AC enables us to construct an object, but AC also proves that this object is unique (up to unique isomorphism if this object is structured).
What about the dimension function $\dim$ which associates to every vector space over $k$ a cardinal number? It is uniquely determined by $\dim(k)=1$ and $\dim(\bigoplus_i V_i) = \sum_i \dim(V_i)$. Remark that the notion of a cardinal number also makes sense in absence of AC; as well as their sum and therefore this function $\dim$. But existence and uniqueness require AC.
Similarily, the transcendence degree $\mathrm{tr.deg}_k$ associates to every field extension of $k$ a cardinal number. If we vary $k$, these are characterized by (1) $\mathrm{tr.deg}_k(k[t])=1$, (2) $\mathrm{tr.deg}_k(E) = \mathrm{tr.deg}_F(E) \cdot \mathrm{tr.deg}_k(F)$ for $k \subseteq E \subseteq F$, (3) $\mathrm{tr.deg}_k(E)=0$ if $E/k$ is algebraic, (4) $\mathrm{tr.deg}_k(\mathrm{Q}(\bigotimes_i R_i)) = \sum_i \mathrm{tr.deg}_k(\mathrm{Q}(R_i))$ if $R_i/k$ are polynomial rings.
To go into a slightly different and probably more interesting direction: Often AC is needed to show that some object has a certain property, although this object can be defined and understood a priori without AC. There are tons of examples in commutative algebra and algebraic geometry, for example:
Let $k$ be an algebraically closed field, for example $\mathbb{C}$. If $X$, $Y$ are integral $k$-schemes, then $X \times_k Y$ is again integral. The affine case is: If $A$, $B$ are $k$-algebras without zero divisors, then the same is true for $A \otimes_k B$. The only proofs I know for this use AC. So in this case, AC also proves the existence of the quotient field of $A \otimes_k B$, which wouldn't make sense if $A \otimes_k B$ wasn't a integral domain.
In linear algebra, you can write down the natural map $i : V \to V^{**}$. It's image $W$ consists precisely of the functionals $V^* \to k$ which are continuous with respect to the weak-*-topology, see Intrinsic description of the image of $V \to V^{**}$. You have to use AC to show that $i$ is injective and therefore construct the inverse map $W \to V$.
I'm not fully satisfied with these examples. I hope someone else finds more natural examples.
A: Ulm's Theorem comes to mind.
This states that any two countable abelian $p$-groups without divisible subgroups have the same Ulm invariants if and only if they are isomorphic. This can, I believe, be proved in ZFC, and relies on choice (though possibly only countable choice). This gives unique (only up to isomorphism) abelian groups and ends up classifying countable abelian torsion groups (to isomorphism).
A: This may be a bit trivial an answer to this (old) question, but since a number of people have reacted with surprise when I mentioned this, and it seems to fall within the purview of what is being asked, let me state:
The Axiom of Choice is equivalent to the following statement:

If $X$ is a set, $\sim$ an equivalence relation on $X$, and $I$ a set, then the obvious map $\Phi\colon X^I/(\sim^I) \to (X/{\sim})^I$ is a bijection.
(Here $X^I$ stands for the set of all $I$-indexed families of elements of $X$ and $\sim^I$ is the equivalence relation which holds between $(x_i)_{i\in I}$ and $(y_i)_{i\in I}$ in $X^I$ iff $x_i \sim y_i$ for all $i\in I$; and $\Phi$ takes the class of $(x_i)_{i\in I}$ to $([x_i])_{i\in I}$, where $[x]$ denotes the class of $x$ mod $\sim$.)

Note that, independently of AC, $\Phi$ is injective by definition of $\sim^I$.
(The equivalence with AC of the above is almost obvious.  If AC holds, then we can lift $(\bar x)_{i\in I}$ in $(X/{\sim})^I$ to a family $(x_i)_{\in I}$ in $X^I$ by choosing a representative for each class.  Conversely, if the above holds and $(Z_i)_{i\in I}$ is a family of inhabited sets, let $X$ be their disjoint union, $\sim$ the equivalence relation for which $Z_i$ is the partition of $X$ so that $X/{\sim}$ is $I$, and use the above to lift the “identity” element of $(X/{\sim})^I = I^I$ to an element of $X^I$ to see that $\prod_{i\in I} Z_i$ is inhabited.)
Thus, in the above context, AC tells us that an injective map $\Phi$ is surjective, or, if we want, that every element in the target has a (necessarily unique) antecedent by $\Phi$.
A: This came up yesterday in my Real Analysis course. I´m not sure if it is the sort of thing you are looking for and I´m also not sure if the use of $AC$ is essential, but….
Suppose $X$ is a complete metric space and $\{E_n:n\in \omega\}$ is a nested sequence of non-empty closed subsets of $X$ such that $\lim_{n \to \infty} \operatorname{diam} (E_n)=0$. Then there is a point $p$ that belongs to every $E_n$.
The only proof I know of this uses countable choice to get a sequence $\{ x_n\}$ with $x_n \in E_n$; then this sequence is a Cauchy sequence, etc.
But then the object whose existence you are trying to prove (i.e. $p$) is unique, by the condition on the diameters.
A: With respect to your second question (I understand the uniqueness requirement in your questions as "being instatiatiated by abstraction terms"):
Suppose that $A$ is equivalent (in $\mathit{ZF}$) to a sentence of the form $\forall z\exists y B$, for $B$ (provably in $\mathit{ZF}$) absolute for transitive models of $\mathit{ZF}$, and that $\mathit{ZFC}\vdash A$.
In this case, $\mathit{ZFC}\vdash\forall x A^{\mathbf{L}(x)}$ (where $x$ is the first variable that does not occur in $A$) if and only if (omitting the quantifier $\forall x$),
$$\mathit{ZFC}\vdash (\forall z\exists y B)^{\mathbf{L}(x)},$$
that is, if and only if
$$\mathit{ZFC}\vdash (\forall z\in \mathbf{L}(x))(\exists y\in \mathbf{L}(x)) B,$$
because $B$ is absolute. If this holds, then
$$\mathit{ZFC}\vdash (x\in \mathbf{L}(x))\rightarrow(\exists y\in \mathbf{L}(x)) B'$$
for $B'$, the formula obtained replacing the free occurrences of $z$ in $B$ by $x$. But then
$$\mathit{ZFC}\vdash (\exists y\in \mathbf{L}(x)) B'$$
and, replacing back $x$ by $z$,
$$\mathit{ZFC}\vdash (\exists y\in \mathbf{L}(z)) B.$$
This means that if $A$ is a theorem of $\mathit{ZFC}$ of the form explained above and such that $\mathit{ZFC}\vdash\forall x A^{\mathbf{L}(x)}$, then $\mathit{ZFC}$ proves that given a set $z$ there exists a set $y$ in $\mathbf{L}(z)$ such that $B$. Therefore, there is a composition of Gödel operations applied to some elements in the transitive closure of $z$ that gives you a witness for that existence. So, even in this simple case you don't have instantiation by an abstraction term with parameter $z$, but you do have something close to it, that is a term with parameters in the transitive closure of $z$. I think that there is no way to substantially improve this.
The so-called existence axioms of set theory are classified according to this condition of being instantiated by an abstraction term or not. The axiom of choice is the example of existence axiom that is not instantiated by an abstraction term. I think that this is an inadequate condition for classifying the axioms and these and other related questions are the subject of my paper "On existence in set theory" in the Notre Dame journal of formal logic.
