Is separation + subset.reflection on transitive sets strong enough to go beyond ZF?

Call this new axiom system $K$.

First, note we can augment the reflection scheme to

$$ \exists x (trans(x) \land set(x) \land (\phi \iff \phi^x))$$

By simply doing case analysis on whether $\phi$ or $\neg \phi$ is true and applying the reflection principle in either case.

Now recall the class comprehension scheme of MK, which consists of all the axioms $A_\phi$ of the form

$$\forall \vec{P}\exists M (\forall x (set(x) \land \phi(\vec{P}, x) \iff x \in M))$$

For any formula $\phi(\vec{P}, x)$ (where $M$ does not appear). I claim each $A_\phi$ is provable from $K$.

For consider some transitive set $t$ such that $A_\phi$ is absolute for $t$. We wish to prove $A_\phi^t$. This formula becomes

$$\forall \vec{P} \subseteq t \exists M \subseteq t (\forall x \in t (\phi^t(\vec{P}, x) \iff x \in M))$$

Take some $\vec{P} \subseteq t$. Then such an $M$ exists by the separation axiom scheme. So we have proved the class comprehension scheme.

With the class comprehension scheme in hand, we can prove the consistency of ZF - Reg in a straightforward way. This is because we can develop the model theory of class-sized models and prove $V \models ZF - Reg$. We can then prove the soundness theorem for class-sized models to conclude that $ZF - Reg$ is consistent.