I have read that $\mathrm{ZF}$ has a transitive model iff it has a countable transitive model. I am interested in generalizations of this result. In particular:
Question. Let $\varphi$ and $\Psi$ denote a sentence and a set of sentences (respectively) in the first-order language of set theory. If $\mathrm{ZF}+\Psi +\varphi$ proves that there exists a transitive model of $\mathrm{ZF}+\varphi$, does $\mathrm{ZF}+\Psi+\varphi$ necessarily prove that there exist a countable transitive model $\mathrm{ZF}+\varphi$?
Addendum. I'm especially interested in the case where the axiom of choice (or a weaker fragment thereof) is an element of $\Psi.$ That being said, the comments suggest that the answer to the full question is "no," so I'd be interested to hear of a counterexample to the full claim.
The answer is yes, in the case that $\sf DC$ is provable from $\sf ZF+\Psi$. The reason is that $\sf DC$ is equivalent to the following instance of the downward Lowenheim-Skolem theorem:
In that case, since $\sf ZF+\Psi+\varphi$ prove the existence of a transitive model $(M,\in)$, it proves there is a countable elementary submodel $N$. Since $(N,\in)$ is well-founded we can collapse it to a countable transitive model $N'$, and since $M, N$ and $N'$ have the same theory, $N'$ is a model of $\sf ZF+\varphi$ as well.
On the other hand, if $\Psi$ is not sufficient to prove $\sf DC$, things become immensely more difficult. The reason is that $\sf ZF+\varphi$ is such a theory, that given any model of $\sf ZFC$ we can produce a model of $\sf ZF+\varphi$ in a way that won't violate transitivity (e.g. forcing, inner models, etc.), in which case if $M$ is a transitive model, we can consider $L^M=L_\alpha$ for some $\alpha$, and we can find a countable ordinal $\gamma$ such that $L_\gamma\prec L_\alpha$, and use $L_\gamma$ to produce a countable transitive model for $\sf ZF+\varphi$.
Well, this is of course not sufficient for actually proving that we can dispense with the axiom of choice here. But the trouble is that in order for this to be true, we need $\varphi$ to be a statement that not only doesn't "reflect nicely" (in the sense that we can find a model of $\sf ZFC$ which we can provably make into a countable model) but is not such statement which we can work from any model of an equiconsistent theory.
For example we can always violate $\sf CH$, we can always violate $\sf AC$ in many ways. Any statement which can be forced, or negated using symmetric models or so, and many other statements of this spirit, all will manage to get through, even though we cannot use $\sf DC$ directly.
(If $\varphi$ is such that $\sf ZF+\varphi$ implies there is a canonical inner model of $\sf ZFC+\varphi'$ which satisfies global choice, and $\varphi$ and $\varphi'$ are equiconsistent, then we can repeat the above argument as with $L^M$.)