A proof can be found here, but it seems that it uses AC. I would like to know if there is a proof for this fact without AC.
I came up with this question after seeing a proof of sequential compactness $\implies$ Compactness for metrizable topological spaces without using generalized Lebesgue's Number Lemma for sequentially compact metric spaces. Both proofs can be found here.