Last night I was thinking about some related statements which follow from ZF+DC, but it actually seems they only need DC to hold in some outer model of the universe. In particular, let $M \models ZF.$ Consider the following claims:

1. For any sentence $\sigma$ such that $M \models \sigma,$ there is a countable transitive model $M_0 \in M$ such that $M_0 \models \sigma.$
2. $L^M$ and $M$ agree on $\Sigma_1$ sentences (Levy's version of Shoenfield absoluteness).
3. $HC^M \prec_1 M.$

I believe these follow from there being some outer model $N \supset M$ where $N \models ZF + DC,$ or even $M$ existing in some ambient universe $V$ such that $V \models ZF+DC \wedge ``M \text{ is transitive}" \wedge \text{ } \omega_1 \subset M.$ E.g., to prove (1), use DC in $V$ to construct a countable transitive model $M_0' \subset M$ such that $M_0' \models \sigma.$ The claim that such a ctm exists is $\Sigma_2^1$ if I'm not mistaken, so Shoenfield absoluteness implies $M$ also has such a ctm.

So I'm wondering if these claims can be proven directly in ZF; I've heard (2) can be, but I've never seen claim (1) proven without DC. Is there a way to formalize "using choice in an ambient universe" within a model? I know there's a theorem of Woodin that says collapsing a supercompact cardinal in a model of ZF forces DC to hold, but that seems overkill.