Working in mono-sorted first order logic with equality $``="$ and membership $``\in"$:
Define: $set(x) \equiv_{df} \exists y \, (x \in y)$
Axiomatize:
Extensionality: $( a \subseteq b \land b \subseteq a \to a=b)$
Separation: $(set(a) \to \exists \ set \ x : \forall y \, (y \in x \leftrightarrow y \in a \land \phi ))$
Reflection: $ \forall \ sets \ \vec{ a_i}, \, \forall \vec {b_i} \ (\varphi \to \exists \ set \ x : \text { trs}(x) \land \varphi^x)$
where formulas $\phi, \varphi$ do not use defined symboles, whose parameters are among $\vec{a_i}, \vec{b_i}$ symbols; $\varphi^x$ is obtained from $\varphi$ by merely bounding all of its quantifiers by $``\subseteq x"$ and replacing each $b_i$ parameter by $b_i \cap x$. $``\text { trs}" $ stands for is transitive.
The idea is to see if this is known to succeed in capturing Bernays reflection schema. Here, the language is mono-sorted, and the idea is if the $\subseteq $ bound and the differential treatment of parameters is enough for that equivalance.
Is the above Reflection equivalent to Bernays reflection (page 21) over the rest of axioms of this theory?