The following theory is another way of dealing with naive comprehension. It uses the double extension principle, broadly speaking similar to what's used in Double Extension Set Theory of Andrzej Kisielewicz (1998), but possibly simpler?
Language: first order logic
Primitives: Equality =, and Two set membership relations $\in_1; \in_2$
Extensionality: for i=1,2: $\forall x,y [\forall z (z \in_i x \leftrightarrow z \in_i y ) \to x=y]$
Define: $\text {uniform}(x) \iff \forall y (y \in_1 x \leftrightarrow y \in_2 x)$
Comprehension: If $\phi^1$ is a formula not using predicate $\in_2$, in which $x$ doen'st occur free, then all closures of:$$ \exists x \forall y (y \in_2 x \leftrightarrow \phi^1)$$; are axioms.
Define: $x=\{y|\phi^1\}^2 \iff \forall y (y \in_2 x \leftrightarrow \phi^1)$
Uniformity: If $\phi^1$ is a formula not using predicate $\in_2$, whose free variables are among $y,x_1,..,x_n$, and $\phi^1(x|y)$ is the formula obtained by merely replacing all occurrences of the symbol $``y"$ in $\phi^1$ by the symbol $``x"$, then all closures of: $$x_1,..,x_n \text { are uniform } \to \\\forall x [x=\{y|\phi^1\}^2 \land \neg \phi^1(x|y) \to \text {uniform}(x)]$$; are axioms.
Induction: over naturals for any formula $\phi$.
Questions:
Is there a clear inconsistency with this theory?
Assuming consistency, what's the strength of this theory?
If we upgrade Induction to Transfinite Induction, would that render the theory inconsistent?