Consider $\phi(A)$ a formula of second-order arithmetic with one free variable $A$ of type "set". Suppose $\exists A : \phi(A)$ is a true sentence. Does it follow (not in second order arithmetic itself, but in a stronger theory of your choice, e.g. ZFC) that there is a formula of second-order arithmetic $\psi(n)$ with one free variable $n$ of type "number", such that $\phi(\lbrace n | \psi(n)\rbrace)$ is a true sentence?