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.