I am talking about the principle that is to DC what the global choice is to the usual axiom of choice. Global choice involves existential quantification over classes, but global DC can be stated as a schema in first-order set theory.

$(\forall x (\phi(x) \to \exists y (\phi(y) \wedge \psi(x,y)))) \to \forall x (\phi(x) \to \exists f (f(0)=x \wedge \forall n \in \omega (\phi(f(n)) \wedge \psi(f(n),f(n+1)))))$

Searching for this I come up with nothing, other than in constructive set theory, where it is called "relativised" DC, and has a simple computational interpretation. I guess that classically, it just follows from ZF+DC. Is that right? I can't figure out how.