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.