The following theory is a fragment of $\small \sf NF$. My question is about if it is known to be consistent ** without** assuming the consistency of $\small\sf NF$.

The language is of first order logic with equality and membership.

**Axioms:**

**1. Extnesionality:** $\forall x \forall y (\forall z ( z \in x \leftrightarrow z \in y ) \to x=y)$

**2. Comprehension:** if $\phi(y)$ is a formula in which $y$ only occurs free, and $x$ not occurring free, having no more than one occurrence of an atomic sub-formula that contains a bound variable in $\phi(y)$ and $y$, and having no more than one occurrence of an atomic sub-formula containing two bound variables in $\phi(y)$, otherwise all atomic sub-formulas must contain a parameter; then all closures of: $$\exists x \forall y (y \in x \leftrightarrow \phi(y))$$; are axioms.

Terminology: by atomic formula here it is meant a formula having exactly two occurrences of variable symbols and one primitive predicate symbol, i.e. either $\in$ or $=$, in between. By *parameters* of a formula $\phi(y)$ its meant any free variable symbol in $\phi(y)$ other than the symbol $``y"$. The primitive logical connectives are the customary four ones and the bi-conditional.

/Theory definition finished.

Now this theory is a fragment of $\small \sf NF$, since all so qualified formulas in comprehension are weakly stratified! IF we in addition allow for the formula to have two atomic sub-formulas with bound variables (instead of one) provided that the total number of variables in those two atomic sub-formulas must be more than two, then we get full $\small \sf NF$.

This theory is not a part of a known fragment of NF like Predicative $\small \sf NF$, nor of Impredicative $\small \sf NF$, nor of $\small \sf NF_3$, nor is of Tupailo's NFSI

My guess is that its very weak and thus consistent.