Halmos in his Naive Set Theory proves that every infinite set has a subset equivalent to $\omega$ using the axiom of choice with its full power. And this leads to the corollary that a set is infinite if and only if it is equivalent to some proper subset of it, which leads to each Dedekind-finite set being finite.
But I've also seen a proof (on Wikipedia) that this can also be proven with just countable choice. However Wikipedia also states that this result is strictly weaker than countable choice.
Question: It is clear that we do require some form of choice, not just ZF, to prove this result.$^1$ But it is even weaker than the countable choice. Can we explicitly state the form of this choice which is equivalent to this result?
$^1$ I've come across the fact that there exists a model of ZF (whatever that means (sorry I've not done any model theory; this is just for your reference)) in which every infinite set is Dedekind-infinite, and yet the countable choice fails.