This is a consequence of ZF as follows.

Assume that all quantifiers of $\varphi$ appear at the front as in the normal forms. Suppose that $\varphi(\vec v)$ has complexity at most $\Sigma_n$ for some large enough $n$. By the reflection theorem, there is a rank-initial segment $V_\kappa$ that is $\Sigma_n$-correct, meaning that all $\Sigma_n$ assertions are absolute from $V_\kappa$ to the full universe $V$. We may assume that $\vec v\in V_\kappa$. So not only is $\varphi$ absolute between $V_\kappa$ and $V$, but also all subformulas of $\varphi$. In particular, if $\varphi$ is true in the full universe $V$, then it will also be true if you bound the initial quantifiers of $\varphi$ by $V_\kappa$, since it doesn't matter for those whether you quantifier over all of $V$ or just $V_\kappa$, as the result is the same. So anterior reflection holds. $$\forall \vec v\ \exists A(A\text{ is transitive and }\varphi\leftrightarrow\varphi^A).$$ The $A$ is simply the next $\Sigma_n$ correct $V_\kappa$ above the ranks of $\vec v$.

This is a consequence of ZF as follows.

Assume that all quantifiers of $\varphi$ appear at the front as in the normal forms. Suppose that $\varphi(\vec v)$ has complexity at most $\Sigma_n$ for some large enough $n$. By the reflection theorem, there is a rank-initial segment $V_\kappa$ that is $\Sigma_n$-correct, meaning that all $\Sigma_n$ assertions are absolute from $V_\kappa$ to the full universe $V$. We may assume that $\vec v\in V_\kappa$. So not only is $\varphi$ absolute between $V_\kappa$ and $V$, but also all subformulas of $\varphi$. In particular, if $\varphi$ is true in the full universe $V$, then it will also be true if you bound the initial quantifiers of $\varphi$ by $V_\kappa$, since it doesn't matter for those whether you quantify over all of $V$ or just $V_\kappa$, as the result is the same by absoluteness. So anterior reflection holds. $$\forall \vec v\ \exists A(A\text{ is transitive and }\varphi\leftrightarrow\varphi^A).$$ The $A$ is simply the next $\Sigma_n$ correct $V_\kappa$ above the ranks of $\vec v$.

This is a consequence of ZF as follows.

Assume that all quantifiers of $\varphi$ appear at the front as in the normal forms. Suppose that $\varphi(\vec v)$ has complexity at most $\Sigma_n$ for some large enough $n$. By the reflection theorem, there is a rank-initial segment $V_\kappa$ that is $\Sigma_n$-correct, meaning that all $\Sigma_n$ assertions are absolute from $V_\kappa$ to the full universe $V$. We may assume that $\vec v\in V_\kappa$. So not only is $\varphi$ absolute between $V_\kappa$ and $V$, but also all subformulas of $\varphi$. In particular, if $\varphi$ is true in the full universe $V$, then it will also be true if you bound the initial quantifiers of $\varphi$ by $V_\kappa$. So anterior reflection holds. $$\forall \vec v\ \exists A(A\text{ is transitive and }\varphi\leftrightarrow\varphi^A).$$ The $A$ is simply the next $\Sigma_n$ correct $V_\kappa$ above the ranks of $\vec v$.

This is a consequence of ZF as follows.

Assume that all quantifiers of $\varphi$ appear at the front as in the normal forms. Suppose that $\varphi(\vec v)$ has complexity at most $\Sigma_n$ for some large enough $n$. By the reflection theorem, there is a rank-initial segment $V_\kappa$ that is $\Sigma_n$-correct, meaning that all $\Sigma_n$ assertions are absolute from $V_\kappa$ to the full universe $V$. We may assume that $\vec v\in V_\kappa$. So not only is $\varphi$ absolute between $V_\kappa$ and $V$, but also all subformulas of $\varphi$. In particular, if $\varphi$ is true in the full universe $V$, then it will also be true if you bound the initial quantifiers of $\varphi$ by $V_\kappa$, since it doesn't matter for those whether you quantifier over all of $V$ or just $V_\kappa$, as the result is the same. So anterior reflection holds. $$\forall \vec v\ \exists A(A\text{ is transitive and }\varphi\leftrightarrow\varphi^A).$$ The $A$ is simply the next $\Sigma_n$ correct $V_\kappa$ above the ranks of $\vec v$.