If every infinite subset has a limit point in a metric space $X$, then $X$ is separable (in ZF) I can prove this in ZFC, but don't know how to prove this in ZF.
Following is the argument of this in ZFC.
Fix $0<r\in \mathbb{R}$ and $x_0\in X$.
Let $A_i = \{x\in X\mid d(x,x_j)\ge r,\, j<i\}$.
Suppose $A_i≠\emptyset$ for every $i\in \omega$.
Then by AC, we can choose $x_i$ for each $A_i$ to derive contradiction.
I want to prove this in ZF. Help.
Additional Question: Does infinite set have a countable subset in ZF? I guess it's true, but I only know the proof in ZFC. (If it is true, I think it would be really useful in many proofs in ZF.)
 A: Unfortunately, the claim is not provable in ZF. 
It is relatively consistent with ZF that there is an infinite Dedekind-finite set of reals, an infinite set of reals $X$ with no countably infinite subset. This set of reals forms a metric space with the usual metric, and it cannot be separable, because it has no countably infinite subset (and no finite subset of an infinite metric space can be dense). 
Meanwhile, such an $X$ has your limit point property. To see this, suppose $Y\subset X$ is infinite, but has no limit point in $X$. In particular, 
every point $y\in Y$ is isolated in $Y$, and therefore we may pick a rational interval neighborhood $(q_x,r_x)$ of $y$ containing no other points from $Y$ except for $y$ itself. We do not need AC to pick this interval, since we may enumerate the rational intervals and pick the first one with this property. Further, each $y\in Y$ gives rise to a distinct such interval. Thus, we have an injective map from $Y$ to the set of rational intervals, and from this it follows that $Y$ is countable, contradicting our assumption that $X$ has no countably infinite subset. 
Note that $X$ also serves as a metric space that is limit-point compact but not compact. We've already shown that it is limit-point compact. But $X$ is not compact because we may simply pick any real $z\notin X$ that is a limit point of $X$, and then use the rational approximations to $z$ to produce an open cover of $X$ with no finite subcover, consisting of intervals straddling these approximations. Thus, ZF (if consistent) does not prove that limit-point-compact metric spaces must be compact.
A: About your second question: IIRC, a set $S$ is by definition infinite iff there is a bijection $f$ from $S$ to a proper subset $T$ of $S$. Now consider a point $x_0\in S\setminus T$, and define $x_n = f(x_{n-1})$. Now if for any $m<n$ we had $x_m=x_n$, then we could apply $f^{-1}$ $m$ times (because it's a bijection) and end up with $x_{n-m}=x_0$. However by construction $x_{n-m}\in T$ and $x_0\in S\setminus T$, thus $x_{n-m}\neq x_0$, and therefore no two $x_n$ are equal. Therefore the set $\{x_n:n\in\mathbb N\}$ is a countable subset of $S$.
