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.