What form of choice is "every Dedekind-finite set is finite" equivalent to?

Question

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.

Answer 1

While answering this question: Strength of “Cofinite Choice”, I discovered that "every Dedekind-finite set is finite" is equivalent to the following "axiom of cofinite choice":

Let $A$ be a set of non-empty sets such that $(\bigcup A)\setminus X$ is finite for all $X\in A$. Then $A$ has a choice function.

See the linked answer for a proof. This seems to me to be a fairly natural choice principle.