Inspired by a recent Math.SE question entitled <a href="http://math.stackexchange.com/questions/10102/where-do-we-need-the-axiom-of-choice-in-riemannian-geometry">Where do we need the axiom of choice in Riemannian geometry?</a>, I was thinking of the <a href="http://en.wikipedia.org/wiki/Arzel%C3%A0%E2%80%93Ascoli_theorem">Arzel&agrave;--Ascoli theorem</a>.  Let's state a very simple version:

> <b>Theorem.</b> Let $\{f_n : [a,b] \to [0,1]\}$ be an equicontinuous sequence of functions.  Then a subsequence $\{f_{n(i)}\}$ converges uniformly on $[a,b]$.

The proofs I have seen operate as follows: Take a countable dense subset $E$ of $[a,b]$.  Use a "diagonalization argument" to find a subsequence converging pointwise on $E$.  Use equicontinuity to conclude that this subsequence actually converges uniformly on $[a,b]$.

The "diagonalization" step goes like this: Enumerate $E$ as $x_1, x_2, \dots$.  $\{f_n(x_1)\}$ is a sequence in $[0,1]$, hence has a convergent subsequence $\{f_{n_1(i)}(x_1)\}$.  $\{f_{n_1(i)}(x_2)\}$ now has a convergent subsequence $\{f_{n_2(i)}(x_2)\}$, and so on.  Then $\{f_{n_i(i)}\}$ converges at all points of $E$.

Of course, to do this, at each step $k$ we had to choose one of the (possibly uncountably many) convergent subsequences of $\{f_{n_{k-1}(i)}(x_k)\}$, so some sort of choice is needed here (I guess dependent choice is enough? I am not a set theorist (IANAST)).  Indeed, we have proved that $[0,1]^E$ is sequentially compact (it is metrizable so it is also compact).

On the other hand, we have not used (equi)continuity in this step, so perhaps there is a clever way to make use of it to avoid needing a choice axiom.

So the question is this:

> Can the Arzel&agrave;--Ascoli theorem be proved in ZF?  If not, is it equivalent to DC or some similar choice axiom?