I agree with Asaf Karagila that the question as literally stated is a bit too sprawling, but you might want to start with Simpson's book, <a href="https://doi.org/10.1017/CBO9780511581007">Subsystems of Second-Order Arithmetic</a>.  Its goals aren't the same as yours, but along the way, the book shows how a large chunk of "countable mathematics" (whatever that means), including analysis, can be developed on the basis of second-order arithmetic (or even in $\mathsf{ACA}_0$), and <i>a fortiori</i> on the basis of ZF. Part of the trick is to avoid "overly general" statements of certain theorems; if you fix certain choices in advance, then you don't have to invoke AC to make those choices on your behalf later, and you can prove versions of (for example) Bolzano&ndash;Weierstrass that suffice for applications.

You might also want to check out <a href="https://mathoverflow.net/a/323754">another MO answer of mine</a> which briefly discusses some other potentially relevant books. Again, they don't have exactly the same goals that you have, but the work they do may be relevant. Here's a quote from Bishop which gives some of the flavor:

> Applications of the axiom of choice in classical mathematics either are irrelevant or are combined with a sweeping use of the principle of omniscience.  The axiom of choice is used to extract elements from equivalence classes where they should never have been put in the first place.  For example, a real number should not be defined as an equivalence class of Cauchy sequences of rational numbers; there is no need to drag in the equivalence classes.</i>

It's harder to avoid AC when it comes to "uncountable mathematics" (whatever that means).  In <a href="https://mathoverflow.net/q/372182">another MO question</a>, I asked whether Hahn&ndash;Banach for $\ell^\infty$ implies the existence of a non-measurable set.  The answer is apparently not well known, and perhaps is not known at all.  From this experience, I infer that analysts by and large have not even bothered to figure out in detail how much functional analysis can be carried out just on the basis of ZF+DC, let alone ZF on its own.