There is an interesting issue with the sentence "(not in second order arithmetic itself, but in a stronger theory of your choice, e.g. ZFC)" inside the question. Even in the cases where the question does have an affirmative answer, that affirmative answer does not mean what it might seem to mean. This is too long for a comment, so I want to make it community wiki. 

The first thought about the meaning of the quote from the question is that we want to prove:

> If $(\exists X)\phi(X)$ is true then there is a formula $\psi(n)$ of second-order arithmetic such that $\text{ZFC}\vdash \phi(\{n : \psi(n)\})$

A moment's reflection shows that this can only work if ZFC proves $(\exists X)\phi(X)$ in the first place. 

So the second thought is that we want to prove: 
> If $\phi(X)$ is a formula of second-order arithmetic such that $\text{ZFC} \vdash (\exists X)\phi(X)$ then there is a formula $\psi(n)$ of second-order arithmetic such that $\text{ZFC}\vdash \phi(\{n : \psi(n)\})$

Now we are getting into the territory of a [witness property][1] for ZFC. 

But there is one more subtlety. What about: 
$$
\phi(X) \equiv (\{0\} = X \land V = L ) \lor (\{1\} = X \land \lnot (V = L) )
$$
Note that $V = L$ here is an abbreviation for ``every real is constructible" which can be expressed as a formula of second-order arithmetic. In this case, we *can* find $\psi$; one possibility is: 
$$
\psi(n) \equiv (0 = n \land V = L ) \lor (1 = n \land \lnot (V = L ))
$$
So we cannot hope for the interpretation of $\psi$ to be absolute, nor can we hope for some sort of extensionality with $\{n : \psi(n)\}$, as the wording of the question might suggest. The set defined by $\psi$ may (necessarily) change from one model to another even though $\psi$ itself stays the same.  Thus our proof in ZFC has to see $\psi$ itself, not just a code for $\{ n : \psi(n)\}$.  



  [1]: http://en.wikipedia.org/wiki/Disjunction_and_existence_properties