This is form 8L of the axiom of choice at http://consequences.emich.edu/CONSEQ.HTM, and is known to be equivalent to countable choice. The proof is fairly straightforward: if $B_1, B_2, ...$ is a countable collection of sets, consider the topological space $X$ consisting of the disjoint union of the $B_i$ with the $B_i$ as a base (the partition topology). This space is separable if and only if there is a choice function.
Qiaochu Yuan
- 118.2k
- 40
- 447
- 741