Does Arzelà-Ascoli require choice? Inspired by a recent Math.SE question entitled 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?

 A: There is a canonical way of checking the literature for most questions of this kind. Since they come up with some frequency, I think having the reference here may be useful.

First, look at "Consequences of
  the Axiom of Choice" by Paul Howard
  and Jean E. Rubin, Mathematical
  Surveys and Monographs, vol 59, AMS,
  (1998). 
If the question is not there, but has
  been studied, there is a fair chance
  that it is in the database of the book
  that is maintained online,
  http://consequences.emich.edu/conseq.htm

Typing "Ascola" on the last entry at the page just linked, tells me this is form 94 Q. Note the statement they provide is usually called the classical Ascoli theorem: 

For any set $F$ of continuous functions 
  from ${\mathbb R}$ to ${\mathbb R}$, the following conditions
  are equivalent:
  1. Each sequence in $F$ has a subsequence that converges
  continuously to some  continuous
  function (not necessarily in $F$ ).
  2. (a) For each $x \in{\mathbb R}$ the set $F (x) =\{f (x) \mid f \in F \}$ is bounded, and
  (b) $F$ is equicontinuous.

To see the other equivalent forms of entry 94, type "94" on the line immediately above. 
From there we learn: Form 94 is "Every denumerable family of non-empty sets of reals has a choice function."
There are some other equivalent forms that may be of interest. For example: 


*

*(94 E) Every second countable topological space is Lindelöf.

*(94 G) Every subset of ${\mathbb R}$ is separable.

*(94 R) Weak Determinacy. If $A$ is a subset of ${\mathbb N}^{\mathbb N}$ with the property that 
$\forall a \in A\forall x \in{\mathbb N}^{\mathbb N}($ if $x(n) = a(n)$ for $n = 0$ and $n$ odd, then $x\in A)$, then in the game $G(A)$ one of the two players has a winning strategy.

*(94 X) Every countable family of dense subsets of ${\mathbb R}$ has a choice function.


Proofs and references are provided by the website and the book. A reference that comes up with some frequency in form 94 is Rhineghost, Y. T. "The naturals are Lindelöf iff Ascoli holds". Categorical perspectives (Kent, OH, 1998), 191–196, Trends Math., Birkhäuser Boston, Boston, MA (2001).
A: I should mention that the theorem
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]$.
holds without any choice (for $a, b \in \mathbb R$). This is proven by using Heine-Cantor for equicontinuous sets and choosing the subsequence in a clever way (see http://arxiv.org/abs/1509.01078 for a proof with a compact subset of $\mathbb R^d$ instead of $[a, b]$; it's not quite short (7 pages), thus I refer to the paper).
The problematic direction is:
Theorem. Let $F \subset \mathcal C(C)$ be sequentially compact ($C \subset \mathbb R^d$ being a compact set). Then $F$ is bounded and equicontinuous.
That's what is equivalent to countable choice for subsets of the real numbers.
