What's the consistency strength of this form of reflection? 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: $ (\varphi \to \exists \ set \ x : \text { trs}(x) \land \varphi^x)$
where formulas $\phi, \varphi$ do not use $``x"$;  $\varphi$ do not use $``="$; $\varphi^x$ is obtained from $\varphi$ by merely bounding all of its quantifiers by $``\subseteq x"$; and $``\text { trs}" $ stands for is transitive.
This theory can prove: Set existence, Empty, Pairing, set Union, Power, Infinity, over the set world of it, also it proves Substitution. It can also prove class comprehension scheme. So it appears to prove all axioms of $\sf MK$-$\sf Reg.$-$\sf Choice$.

Is this theory consistent?


If so, is it equivalent to Bernay's reflection?

 A: This theory is inconsistent.
We note that by 1 and 2 that if set(x) and y⊆x, then set(y).
(a) There is a v such that ∀x(set(x)-->x∈v).
Proof:Suppose not. Then ∀v∃s∃t(s∈t∧s∉v). By 3 there is transitive x such that
  set(x) and ∀v(v⊆x-->∃s∃t(s⊆x∧t⊆x∧s∈t∧s∉v). In particular 

  (x⊆x-->∃s∃t(s⊆x∧t⊆x∧s∈t∧s∉x).  But this is impossible.

Suppose that ∀x(set(x)-->x∈V). Then ∃w∀t(t∈V-->t∈w). By 3 there is transitive x
such that set(x) and ∃w(w⊆x∧∀t(t⊆x∧t∈V-->t∈w)). Since t⊆x implies set(t),
t⊆x implies t∈x. By 2, there is a c such that t∈c<-->(t∈x∧t∉t). Since set(c),
c∈c<-->c∉c.
A: Here is a partial answer to the second question.
This theory does prove Bernays Reflection axiom, which I think can be stated as: $$ \forall a_1,...,\forall a_n (\varphi(a_1,..,a_n) \to \\\exists \ set \ x : \text { trs}(x) \land \varphi^x(a_1 \cap x,...,a_n \cap x))$$
Where $\varphi$ doesn't use $x$, and all of its free variables are among $a_1,..,a_n$. The other specifications remain the same except that $\varphi$ can use equality.
To see that, we take any formula $\varphi(a_1,..,a_n)$, then form the formula: $$\exists b_1,.., \exists b_n: b_1 \equiv a_n , .., b_n \equiv a_n \land \varphi(b_1|a_1,..,b_n|a_n)$$ Where $\equiv$ is the co-extensionality relation, i.e.; $a \equiv b$ is the formula $ \forall m \, (m \in a \leftrightarrow m \in b)$; and $b_i | a_i$ means that each $b_i$ replaces only and all the occurrences of $a_i$ in formula $\varphi(a_1,..,a_n)$. The intention is to have: $b_i = a_i \cap x$ upon reflecting the $b_i$'s on $x$. This is because each $b_i \equiv a_i$ would turn upon reflecting it on $x$ to: $\forall m \subseteq x \, (m \in b_i \leftrightarrow m \in a_i)$ and beforehand we already have each $b_i \subseteq x$, and since now we have all elements of $a_i$ that are subsets of $x$ being elements of $b_i$, so we have $b_i = a_i \cap x$, regarding the use of equality between two bound variables in $\varphi$, then those upon reflection on $x$ would be subsets of $x$, and so co-extensionality over them would be equivalent to equality between them (Extensionality and equality theory). So Bernays schema is provable in this theory. The problem is whether this theory is even stronger? Or even not consistent?
