Is the Axiom of Choice necessary in the proof that any subset of a metric space that contains its limit points is closed? Let $(X,d)$ be a metric space and $U$ a subset of $X$. It is an elementary fact that $U$ is closed in $X$ if and only if it contains all its limit points. The forward direction is proven by showing that if there's a limit point in $X \backslash U$ then $X \backslash U$ is not open, so $U$ is not closed. 
The backward direction is what my question is about. We show that if $U$ is not closed then it doesn't contain all its limits points. If $U$ is not closed then $X\backslash U$ is not open. So there is an $x\in X \backslash U$ such that for any $n\in \mathbb{N}$ the ball $B\left(x,\frac{1}{n}\right)$ intersects $U$. Therefore for each $n$ we can choose an $x_n$ in this (infinite) intersection and then the sequence $(x_n) \subset U$ converges to $x$, so we have a limit point $x\notin U$. Now my knowledge of exactly when the Axiom of Choice is necessary in mathematical arguments is limited but to me it seems like we are using it here to construct the sequence. Is it necessary here or is there some way to circumvent this? It would be strange if the Axiom of Choice was necessary for such a basic, standard property of metric spaces. 
 A: It's exactly equivalent to the axiom of countable choice, which is vastly weaker than the full axiom of choice:

ACC: every countable family $(X_i)_{i\in\mathbb{N}}$ of nonempty sets has a choice function.

Here's a rough argument for their equivalence:


*

*The usual proof of the result in the OP just uses ACC: given a non-closed subset $S$ of a metric space $M$, we pick some point $x$ in $cl(S)\setminus S$; letting $X_i=\{t\in S: d(t,s)<{1\over 2^n}\}$, any choice function for $(X_i)_{i\in\omega}$ gives a sequence from $S$ converging to $x$. So non-closed sets are non-sequentially closed.

*Conversely, suppose $\mathcal{X}=(X_i)_{i\in\mathbb{N}}$ is a counterexample to ACC. Look at the "partial products" - let $Y_i=X_1\times X_2\times ...\times X_i$. We'll say more about why the shift from $X_i$s to $Y_i$s is needed below. Create a new metric space with domain $M=(\bigsqcup_{i\in\mathbb{N}}Y_i)\sqcup\{\infty\}$ and metric satisfying $d(\infty, x)={1\over 2^i}$ whenever $x\in Y_i$ (we don't care what else the metric does). The set $S=M\setminus\{\infty\}$ isn't closed, but from any sequence $\sigma$ from $S$ converging to $\infty$ we can get a choice function for $\mathcal{X}$: we first "thin" our convergent sequence to get a sequence $\hat{\sigma}=(\alpha_i)_{i\in\mathbb{N}}$ with $\alpha_i\in Y_{k_i}$ with $k_i<k_{i+1}$, and now "throw away" terms from redundant $X$-parts: e.g. if $\hat{\sigma}$ begins $$(a_1^1),(a_1^2,a_2^2),(a_1^3,a_2^3,a_3^3,a_4^3,a_5^3),(a_1^4,a_2^4,a_3^4,a_4^4,a_5^4, a_6^4, a_7^4),...$$ (so $k_1=1, k_2=2, k_3=5, k_4=7, ...$), we would produce the sequence $$(a_1^1, a_2^2, a_3^3, a_4^3, a_5^3, a_6^4, a_7^4, ...).$$


*

*Why did we need to pass to the $Y$s? Well, if we ran the analogous construction with just the $X$s, a sequence wouldn't necessarily give us a full choice function: it would give us an infinite subset of a choice function since some of the $X_i$s might be "skipped" (repetition isn't a problem, just choose the "first point" hit). Bringing in the $Y$s forces any sequence to "generate enough information" to get a whole choice function. (Incidentally, this same trick shows that ACC is equivalent to its "infinitely often" version - the at-first-glance-weaker principle "for every countable family of nonempty disjoint sets $(X_i)_{i\in\omega}$, there is a set $A$ such that for infinitely many $i$ we have $\vert A\cap X_i\vert=1$.")


