set theory - Choice function for Borel sets?

As Simon pointed out, you can't do this without some use of choice. However, you can "almost" do it: the trick is to work with codes for Borel sets instead of actual Borel sets (when you can).

Let $S subseteq mathbb{R}timesmathbb{R}$ be a universal analytic set, i.e. $S$ is analytic and for every analytic set $A subseteq mathbb{R}$ there is a $x$ such that $A = S_x = { y in mathbb{R} : (x,y) in S }$. By the Jankov–von Neumann Uniformization Theorem (which is provable in ZF), the set $S$ has a uniformizing (partial) function $f:mathbb{R}tomathbb{R}$, i.e. $mathrm{dom}(f) = { x in mathbb{R} : S_x neq varnothing }$ and ${(x,f(x)) : x in mathbb{R}} subseteq S$. Since every Borel set is analytic, this $f$ gives you what you want provided you know codes $x$ such that the $S_x$ are Borel sets you're interested in. Picking a unique code for each Borel set is a difficult task which requires some choice. However, you can invoke the Axiom of Choice once to get such a function that gives unique codes and keep working with that function until the end of time, thereby avoiding repeated uses of choice.

See, for example, Kechris's Classical Descriptive Set Theory (II.18) for details on the Jankov–von Neumann Uniformization Theorem, and many other useful uniformization theorems (Kuratowski–Ryll Nardzewski, Kondô–Novikov, etc) that can be used in a variety of contexts.