Working in mono-sorted first order logic with equality and membership:

• Define: $\operatorname{set}(x) \equiv_\text{df} \exists y \, (x \in y)$

• Axiomatize:

1. Extensionality: $(\forall x \, (x \in a \leftrightarrow x \in b) \to a=b)$

2. Separation: $(\operatorname{set}(a) \to \exists \ \text{set $x$} \, \forall y (y \in x \leftrightarrow y \in a \land \phi))$

3. Reflection: $\forall \vec{ b} \, \forall \ \text{sets $\vec{p}$} \ (\varphi \to \exists \text { trs } x : \operatorname{set}(x) \land \varphi^x)$

“trs” stands for is transitive; formulas $\phi, \varphi$ doesn't use “$x$”; $\varphi$ only has $\vec{p}$, $\vec{b}$ as its free variables, doesn't use defined predicates, but allows the use of function symbols only if defined from objects to sets without having class arugments other than from parameters $\vec{b}$; and parameters $\vec{b}$ can only occur in $\varphi$ as arguments of function symbols; $\varphi^x$ is the formula obtained from $\varphi$ by merely bounding all of its quantifiers by “$\subseteq x$”.

Now this theory straighforwardly prove all axioms of ZF − Regularity over the set realm of it.

The idea is to allow class parameters over $\varphi$ in Reflection without the need to re-interpet them in $\varphi$ by their intersections with $x$ in $\varphi^x$ as its used in Bernays reflection axiom schema. The hope is to smuggle them through the set function term symbols thereby circumventing the reflective process as regards them.

I'm not sure if this trick is safe. But if so, then this would provide a way of insinuating class parameters into reflection without them being altered, which is powerful enough to directly prove replacement, as well as existence of inaccessibles, so it goes beyond ZFC in consistency strength.

Can this theory be consistent? And can it be as strong as Bernays reflection?