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:

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:

Now we are getting into the territory of a witness property 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)\}$.

Edit: I have expanded my original post somewhat. It's still marked as community wiki.

The question can be read in several ways, depending on the order in which the quantifiers are ordered. The answer by Emil Jeřábek addresses the following interpretation:

Does ZFC prove the following: "For every formula $\phi(A)$ of second order arithmetic there is a formula $\psi(n)$ of second order arithmetic such that $(\exists A)\phi(A) $ implies $\phi(\{n : \psi(n)\})$".

That is one reasonable interpretation of the question. But it is not the interpretation I had in mind when I read the question, because the formula $\phi$ is chosen before any mention of ZFC.

This is an particularly common issue in proof theory: there is an important difference between "if $\phi(A)$ is a true formula of second-order arithmetic, then ZFC proves ..." and "ZFC proves that if $\phi(A)$ is true a formula of second-order arithmetic, then ...".

When I read the question, it struck me as asking about something like the witness property that is commonly considered in constructive mathematics. The witness property theory for a theory with a particular language of formulas $L$ and a particular language of terms $T$ says that if the theory proves $(\exists X) \phi(X)$ for some $\phi(X) \in L$ then the theory proves $\phi(t)$ for some term $t \in T$.

For example, higher-order Heyting arithmetic has the term existence property for formulas with one free natural number variable and terms of the form $S(S(S(\cdots S(0)\cdots)))$ from the language of arithmetic.

I will explain my reading of the question, and then I will explain why it has a negative answer (with no additional set theoretic hypotheses in the metatheory). If this was not the question that was intended, it is still an interesting (although somewhat trivial) result, in my opinion. It fits with the general intuition that classical theories are not likely to have strong witness properties.

An alternative reading of the question

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

A moment's reflection shows that this can only work if ZFC proves $(\exists X)\phi(X)$ in the first place. So it appears that we want to prove:

Now we are getting into the territory of a witness property for ZFC. The language of formulas consists of all second-order formulas with one free set variable; the term language consists of terms of the form $\{n : \psi(n)\}$ where $\psi(n)$ is a formula of second order arithmetic.

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)\}$.

But we will show that the overall question has a negative answer anyway.

Negative answer

Using a construction similar to the answer by Emil Jeřábek, let $\phi(A)$ say: "If there is a nonconstructible real then $A$ is a nonconstructible real". Clearly $\text{ZFC}\vdash (\exists A)\phi(A)$. But there can be no $\psi$ such that $\text{ZFC} \vdash \phi(\{n :\psi(n)\})$, for the same reason as the negative answer in that other answer. If we look at the particular model of ZFC in which $V$ is a Cohen forcing extension of $L$, then no $\psi$ can define a nonconstructible real in that model.

There is some restriction in the counterexample $\phi$ we could use here. Because of Shoenfield's absoluteness theorem, ZFC does have witness property in question for formulas that are sufficiently low in the analytical hierarchy. For such formulas, ZFC proves that if $(\exists A)\phi(A)$ then $(\exists X \in L)\phi(A)$ and then $\psi$ can be a formula which defines the least set, under the $\Delta^1_2$ well ordering of $L$, which satisfies $\phi$.