Theorem: Let $M$ be a Cauchy complete metric space. Suppose we have a sequence of non-empty closed sets $A_1 \supseteq A_2 \supseteq \cdots$ such that $\text{diam}(A_n) \rightarrow 0$. Then $\cap_n A_n$ is a singleton.
The proof is a straightforward application of the Axiom of Countable Choice. I'm interested in tracking how this invocation of Choice affects the rest of analysis. I have done some research of my own, but haven't been able to find much.
What results in analysis are proven using this theorem?
Can this theorem be proven using a weaker form of Choice? Or, if possible (but I highly doubt it), no Choice at all?