Separable Hahn-Banach and the axiom of choice

We had in our functional analysis course a proof for the Hahn-Banach theorem on a separable Banach space which doesn't need, according to our professsor, the axiom of choice. Yesterday I read the proof again and I am not sure if we really don't need the AC.

The proof starts with:

"Let $\{ x_1, x_2, \dots \}$ be a countable dense set."

And this is exactly the point I am confused about. The definition of a separable space just gives us the existence of countable dense sets but not a concrete one. Don't we need, in general, the axiom of choice for choosing a concrete set?

• No, we do not. If a set is nonempty, picking an element of the set is not using the axiom of choice. This is just a valid line of reasoning. (In first order logic this can be formalized for instance via the rule of existential instantiation.) – Andrés E. Caicedo Dec 17 '14 at 19:13
• (On the other hand, you'd be using the axiom of choice if you were giving an infinite family of (arbitrary) separable Banach spaces and needed to pick countable dense subsets from all of them.) – Andrés E. Caicedo Dec 17 '14 at 19:15
• @AndresCaicedo: I think you should post these comments as an answer. – PhoemueX Dec 17 '14 at 19:50

Just like you can say "let $$x$$ be a real number", or "let $$a$$ be a polynomial in $$R[x,y,z]$$", you can say "let $$A$$ be a dense set".
Once you know that something exists, you can instantiate it and "pick one". The axiom of choice has nothing to do with that. In this case, a countable dense open set. We can just pick one. Then, because it is countable, the collection of enumerations is non-empty, so we can again pick one, so we can just write the set as $$\{x_n\mid n\in\Bbb N\}$$. No choice needed.