Does second-order arithmetic prove every expressible instance of Dependent Choice? Let bigset(X) and rel(X,Y) be otherwise arbitrary formulas in the language of second-order arithmetic with the indicated variables free, and thmemberof(Z,x,X) be the formula asserting that X is the xth member of the sequence of sets coded by Z.  Does it follow that second-order arithmetic proves
$((\exists X)(bigset(X)) \; \land \; (\forall X)(bigset(X) \implies (\exists Y)(bigset(Y) \; \land \; rel(X,Y)))) \implies$
$(\exists Z)(\forall x)(\exists X)(\exists Y)($
$bigset(X) \; \land \; bigset(Y) \; \land \; thmemberof(Z,x,X) \; \land \; thmemberof(Z,\operatorname{S}(x),Y) \; \land \; rel(X,Y))$
?

By second-order arithmetic, I mean Robinson arithmetic + full comprehension + the second-order induction axiom.
 A: Carl has pointed out that my previous answer missed a clause in the theorem I cited.
Simpson's book, Subsystems of Second Order Arithmetic, does address this in section VII.6.  He shows that dependent choice for $\Sigma^1_2$ formulas is equivalent to $\Delta^1_2$ comprehension plus $\Sigma^1_2$ induction (Theorem VII.6.9).
However even regular (non-dependent) $\Sigma^1_3$ choice is independent of full comprehension; he attributes this result to Feferman and Levy, and cites Theorem 8 of Levy's "Definability in axiomatic set theory, II".  
The result I mentioned before, that $\Sigma^1_k$ dependent choice is equivalent to $\Delta^1_k$ comprehension plus $\Sigma^1_k$ induction for $k\geq 2$, holds for $k\geq 3$ requires the additional assumption that the universe is constructible from from some set of integers.
Your statement of dependent choice is a bit more complicated than necessary; you can fold bigset into rel (take $rel'(X,Y)$ to hold if either $\neg bigset(X)$ and $bigset(Y)$, or if $bigset(X)$, $bigset(Y)$, and $rel(X,Y)$).  Conversely, it's a bit simpler than the version Simpson uses (which I believe is standard), in which $rel$ can depend on the parameter $x$ as well.
