# Choice of a real number using the axiom of choice

I wonder if one can define the axiom of choice by the assumption that is possible to choose an arbitrary real number?

If we define real numbers as Cauchy limits of rational numbers, I assume that we must consider that as a set, since it is a case of so called actual infinity, referencing directly an infinite number of limits.

In any case that would just mean choosing one element out of one set, rather than involving an infinite number of sets, in what you see in the formal definitions.

My question is therefore: is the formal – complicated - definition absolutely necessary?

Edit: Based on the answer by Asaf Karagila I realize I was hasty with the reals. I expect I can mend it, either by accepting the equivalent classes of limits of Cauchy series, or by restricting the series by using infinite (decimal) expansions and the added rule that series of 1000….has priority over 0999… (these series containing 0999… are then discarded ) which I believe would make the definition unique.

Choosing one element from a provably non-empty set requires no appeal to the axiom of choice, but rather an appeal to the laws of your logic. Specifically, existential instantiation. If $\exists x\varphi(x)$ is provable; then we can add a new constant symbol to the language $c$ and the statement $\varphi(c)$.