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?

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.

What may confuse you here is that we chose an infinite set. So it seems like we somehow made infinitely many choices, but in fact, we only made two: first we chose a countable dense set, then we chose an enumeration.