Inspired by a recent Math.SE question entitled Where do we need the axiom of choice in Riemannian geometry?Where do we need the axiom of choice in Riemannian geometry?, I was thinking of the Arzelà--Ascoli theorem. Let's state a very simple version:
Theorem. 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à--Ascoli theorem be proved in ZF? If not, is it equivalent to DC or some similar choice axiom?
