Is there a theorem that guarantees the existence of a proof not using AC given there is a proof using AC, at least under some circumstances? What is its name (if there is one) and its most general form?
This of course excludes the trivial cases for example a finite collection of non-empty sets.
There are important such results, for example the Shoenfield Absoluteness Theorem.
Among other things, it shows that any $\Pi_2^1$ sentence of Peano Arithmetic that (with the usual translation) can be proved in ZFC can already be proved in ZF. (That had already been shown much earlier by Gödel. Shoenfield's result is stronger.) The $\Pi_2^1$ sentences include well-known open problems such as the Goldbach Conjecture, the Riemann Hypothesis, $\text{P}=\text{NP}$, many more.