The proof that you suggest does not require the axiom of choice, as several people have pointed out.
However, other proofs do use the axiom of choice in a very subtle and implicit way. For example, every infinite set has a countably infinite subset is a statement which requires the use of the axiom of choice (or a different definition for "infinite").
Another important example would be that if we define a sequence recursively by simply showing that at each step "there is a way to continue to sequence", then there is a sequence which satisfies the construction.
A common place where this sort of argument is used is in analysis or topology, when arguing that in a metric space (e.g. $\Bbb R$), if $x$ is in the closure of $A$, then there is a sequence from $A$ converging to $x$. Simply at each step take a point closer than the last one you've taken. Another would be in arguing that in a finitely-splitting tree with infinitely many levels there is an infinite branch: at each step there is a node extending the branch you have so far, such that this node has infinite many points above it.
Henning said, and correctly so, that modern mathematician are not excited by using the axiom of choice. It is a good and useful axiom when it comes to managing the infinite.
The axiom of choice is not "leaking" into everyday mathematics, it was always there to some extent. When the French school of Lebesgue and Borel objected the use of the axiom of choice, they were implicitly using it themselves. As the methods for proving independence of logical statements in a set theoretic context were developed into the 1960s we saw that in fact a great deal of statements that are seemingly naive require the axiom of choice.
How naive? Well, naive enough that without them developing the notion of Borel sets become meaningless, let alone the Lebesgue measure. In an ironic twist of poetic justice, those who argued so thoroughly against using the axiom of choice were using it themselves all along.
(One could make the case that something like Dependent Choice is "good" and "uncountable choice" is evil, but there are things to say about that just as well.)
In any case, mathematicians saw that assuming the axiom of choice does not lead to [logical] contradictions, and they started to embrace it even deeper. The result, now, 80 years after Gödel's constructible universe, is that a few generations of mathematicians were educated upon results using the axiom of choice, and this sort of mathematics is ingrained in our "everyday mathematics".
And as it is always the case, after a few generations, some things simply become "fact". The standard of what we call "proof", the incompleteness phenomenon of mathematics, and just as those, the axiom of choice itself, are part of the subliminal mathematics that we take almost for granted when we think about mathematics. Even if sometimes we stop to think about those things are get confused and baffled.