Isomorphic Free Groups and the Axiom of Choice

When I read about free group, the proof which concerns about two free groups $F(X)$ and $F(Y)$ are isomorphic only if $\operatorname{card}(X) = \operatorname{card}(Y)$ has a sentence going as follows:

$|M(X \cup X^{-1})|=|X \cup X^{-1}|=|X|$, using the axiom of choice.

Can someone give me more hint about this question or some references?

Solutions Collecting From Web of "Isomorphic Free Groups and the Axiom of Choice"

This is mentioned (and proved) in the second page of the following paper,

Herbert Federer and Bjarni Jonsson, Some Properties of Free Groups. Transactions of the American Mathematical Society, Vol. 68, No. 1 (Jan., 1950), pp. 1-27.

Some three decades later this was also addressed in the following paper (Problems 4 & 5),

Paul E. Howard, Subgroups of a Free Group and the Axiom of Choice. The Journal of Symbolic Logic, Vol. 50, No. 2 (Jun., 1985), pp. 458-467.

The formulation of the open problems indicate that at the time of writing absolutely nothing was known, whether or not the isomorphism type of the group determines the cardinality of its generators (the first problem is whether or not this is provable without choice, the second problem is whether or not it implies full choice).

Howard’s paper does not seem to be referenced elsewhere, so I am willing to believe this is still open.

EDIT (April 2015).

I recently found a paper that was published a year ago,

Philipp Kleppmann, Generating sets of free groups and the axiom of choice. Mathematical Logic Quarterly, Vol. 60, No. 3 (2014), 239–241.

The author proves there that $F(X)\cong F(Y)\iff |X|=|Y|$ is provable from the Boolean Prime Ideal theorem, and therefore does not imply the axiom of choice.

However, the assumption that $|F(X)|=|F(Y)|\iff |X|=|Y|$ for every infinite $X,Y$, does in fact imply the axiom of choice.

If $u_1 \ldots u_n$ is the writting of a element of $F(X)$, how many elements have a writting of the form $u_1 \ldots u_n v$ ?

Starting from here, you have a recursion relation $|W_{i+1}| = f( |W_i| )$ where $W_i$ is the elements of $F(X)$ with writting of length $i$. Then, you can deduce $|F(X)| = |\bigcup_{i \in \mathbb N} W_i|$ with respect to $|X|$.

(As someone noted in the comments, your proof is only relevant when $|X| > \aleph_0$.)