set theory - Is Dependent Choice all we really need?

Let me adopt an extreme interpretation of your question, in order to prove an affirmative answer.

Yes, in the arena of the countable, DC suffices.

To see why, let me first explain what I mean. If one wants to consider only countable sets, then the natural set-theoretic context is HC, the class of hereditarily countable sets. These are the sets that are countable, and all members are countable, and members-of-members and so on. The class HC is the land of all-countable set theory, the land of the fundamentally countable. I am not proposing that you want to remain within HC. Rather, you want to consider the properties of the objects in HC that are expressable there and what you can prove about them in ZF+DC, versus ZFC.

Since hereditarily countable sets can be coded easily by real numbers, it turns out that the structure HC is mutually interpreted in the usual structure of the reals R and vice versa. That is, the structure HC is essentially equivalent in a highly concrete way to the usual structure of the real numbers. And so questions about the fundamentally countable are equivalent to questions in the usual projective hierarchy of descriptive set theory. Thus, in this interpretation, your question is really asking whether one needs ever needs AC as opposed to DC in order to prove a projective statement.

Question. Are the projective consequences of ZFC the same as those of ZF+DC?

The answer is Yes, by the following theorem.

Theorem. A projective statement is provable in ZFC if and only if it is provable in ZF+DC.

Proof. It suffices to show that for every model W of ZF+DC there is a model of ZFC with the same reals. The reason this suffices is that in this case, any projective statement failing in a model of ZF+DC will also fail in a model of ZFC.

So, suppose that W is a model of ZF+DC. Let L(R) be the inner model of W obtained by constructing relative to reals. This is also a model of ZF+DC. Consider the forcing notion P in L(R) consisting of well-ordered countable sequences of real numbers in L(R), ordered by end-extension. Let G subset P be L(R)-generic for P. Since P is countably closed in L(R), it follows that the forcing extension L(R)[G] has no additional real numbers. And since G adds a well-ordering of these reals in order type &omega₁, it follows that L(R)[G] has a well-ordering of the reals. From this, it follows that L(R)[G] is actually a model of ZFC, since it has the form L[A], where A is a subset of &omega₁ enumerating these reals in the order that G lists them. Thus, we have provided a model of ZFC, namely L(R)[G], with the same reals as W. It follows that W and L(R)[G] have the same projective truth, since this truth is obtained by quantifying only over this common set of reals. QED

This phenomenon generalizes by the same argument beyond projective statements, to statements of the form "L(R) satisfies phi". The point is that ZFC and ZF+DC prove exactly the same truths for L(R), since any model W of ZF+DC has the same L(R) as the model L(R)[G] in the proof above, and this satisfies ZFC.

The conclusion is that if you wish to study mathematical objects that are essentially countable only in the weak sense that they exist in L(R)---and this includes many highly uncountable objects---then the features about them in L(R) that you can prove in ZFC are exactly the same as the features you can prove in ZF+DC. So this interpretation is not so extreme after all...