Let **Anterior Reflection** be the following principle: $$\forall \vec{v}~ \exists X: \operatorname {transitive} (X) \land \, (\varphi \to \varphi^{X"}) $$

where $\varphi$ is a formula in $\sf FOL(=,\in)$ that doesn't use the symbol $X$, and $\varphi^{X"}$ refers to $\varphi$ being *anteriorly bounded* by $X$, that is a formula obtained from $\varphi$ by merely bounding *some* of its quantifiers by $X$ in such a manner that all preceding quantifiers (i.e. appearing on the left of it) must be bounded by $X$ also, i.e. the bounding by $X$ is closed anteriorly.

Note: bounding is of the form $\exists y \in X, \forall z \in X$.

Clearly, Anterior Reflection together with Specification principle would axiomatize $\sf ZF–Reg.–Powerset$, where Specification is: $$\forall \vec{v} ~ \forall A ~ \exists! x ~ \forall y ~ (y \in x \leftrightarrow y \in A \land \varphi) \text{ ;}$$ for every formula $\varphi$ not using the symbol "$x$".

If we upgrade anterior reflection to work on supertransitive sets, then with specification we get $\sf ZF–Reg.$.

Now, I think this is consistent.

What is the proof of consistency of anterior reflection?