Background
The reflection principle is a theorem schema in ZF. Given a formula $ φ $ and a set $ M $ we obtain $ φ $ relativized to $ M $ by restricting all quantifiers of $ φ $ to range over $ M $. We denote this as $ φ^M $. We will say that $ M $ reflects $ φ $ if $( φ^M ⇔ φ) $.
reflection principle: For every formula φ of ZF, the following holds in ZF:
$∀x∃α(x ∈ V_α ∧ V_α \text{ reflects } φ)$.
Question
Does an external version of the reflection principle exist in Internal Set Theory (as formulated by Edward Nelson)? Extending theorem schemas is not a trivial matter. We have seen for the induction schema that it does not hold for external formulas, but found an external replacement instead. Is there a proof of the following theorem in IST? And if not, which external formula cannot be reflected in this manner, and is there perhaps a weaker version of the theorem?
external reflection principle: For every (external) formula φ of IST, the following holds in IST: $∀x∃α(x ∈ V_α ∧ V_α \text{ reflects } φ)$.
Attempts made
I have tried to adapt different proofs of the reflection principle to IST (for instance the one found in ebbinghaus, similar to this but with predicates instead of classes), but all of them seem to require replacement or separation of external formulas, which is illegal set formation in IST. At the same time I have found no counterexamples. Other attempts have been trying to find some external proof using standardization in particular, or trying to use the reduction to go from the internal to external case (this last approach seems undoable to me because of the possible free variables)