I have preoccupied myself some with very weak set theories that suffice to interpret Robinson Arithmetic, as in this question Is Extensionality needed for the incompleteness of very weak set theories?. May we have confidence that the theory SU, which has the axioms for empty set and for universal set and for adjunction as well as the rules $\vdash\hspace{-2pt}\alpha(a)\Leftrightarrow\hspace{2pt}\vdash\hspace{-2pt} a\notin\{x|\lnot\alpha(x)\}$ and $\vdash\hspace{-2pt}\alpha(a)\Leftrightarrow\hspace{2pt}\vdash\hspace{-2pt} a\in\{x|\alpha(x)\}$ is consistent or even omega consistent in an appropriate sense? Does SU still support its own coding to get a Godelian provability predicate for SU?

SU has all set terms and we presuppose an underlying theory of identity by having the Leibnizian-Russellian definition of $a=b$ as $\forall u(a\in u\rightarrow b\in u)$ and the axiom schema $\vdash\forall x, y(x=y\rightarrow(\alpha(x)\rightarrow\alpha(y)))$.

P.S. The appropriate omega consistency I want is that if $\vdash\alpha(t)$ for all terms $t$ then $\nvdash\exists x\lnot\alpha(x)$.