Here is a model of your theory. Start with a countably infinite set of objects $X=\bigsqcup_n X_n$, partitioned into infinitely many infinite sections. We inductively define $\in_n$. Consider the various formulas $\phi^n(y,z)$ that use only at most $\in_m$ for $m<n$, with parameters $z$. With the various possible parameters $z$, these define certain subsets of $X$, but only countably many. For each such definable subset, which has not already arisen earlier, assign an object $x$ from $X_n$ to represent it, and define $y\in_n x\iff\phi^n(y,z)$ for this instance. That is, I pick the object to represent the set for each definable set, not for each formula. Thus, we will satisfy comprehension. If the definable set had already occurred at an earlier stage $m<n$, then I use the same object $x\in X_m$ as previously, and define $y\in_n x$ for the same members $y$. The effect of this is that whenever $y\in_n x$ then $y\in_k x$ for all $k\geq n$, since I can always add a vacuous use of $\in_k$ to any formula and define the same set at a higher level. So the level doesn't matter, once you are in the set. This will give us the membership axiom. And since I was careful always to reuse the old object whenever the definable set is the same, we will get extensionality. This method of argument is rather similar to some of the solutions of Frege's Basic Law V for first-order definability, as discussed in my paper - [Fregean abstraction in Zermelo-Fraenkel set theory: a deflationary account](https://mxphi.com/wp-content/uploads/2023/10/HA.pdf), Annals of Mathematics and Philosophy, 2023. (arxiv:[2209.07845](https://arxiv.org/abs/2209.07845)) See the prior art section there, where I discuss this method, used in various work by Parsons, Bell, and Burgess. In particular: - Terence Parsons. “On the consistency of the first-order portion of Frege’s logical system”. Notre Dame J. Formal Logic 28.1 (1987), pp. 161–168. ISSN: 0029-4527. DOI:[10. 1305/ndjfl/1093636853](https://doi.org/10.1305/ndjfl/1093636853). One can perform the construction over any given model already. That is, we can assume $X$ already has some other first-order structure, but then chop it into the sections and undertake this construction on top of it, allowing formulas $\phi^n$ in the full language. This is essentially how the Parsons method works.