Is this fragment of NF known to be consistent?

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.

• If you believe Randall's proof, then all the fragments of NF are consistent... – Asaf Karagila Jun 6 '19 at 9:26
• @AsafKaragila, that's why I asked for a proof that is independent of consistency of NF, if this fragment is strictly weaker than NF, then it must be the case that it can be proved consistent without the need for consistency of NF. Holmes's proof of NF is monstrously complex, so I've asked here for a proof that doesn't depend on that. – Zuhair Al-Johar Jun 6 '19 at 10:03
• I'm having difficulty parsing your restriction on comprehension. Could you give some examples of formulas that are and are not allowed? – James Hanson Jun 6 '19 at 20:41
• @JamesHanson, Nice, please look at the link to full NF that I've wrote (end of fourth line from below), there all the defining formulas are examples of that comprehension EXCEPT the formula of the axiom of "Product" because it contains two occurrences of atomic subformulas with solely bound variables that are $z, r, s$, – Zuhair Al-Johar Jun 6 '19 at 21:19
• In nutshell in order to know which formula is allowed you just examine its atomic subformulas, those should contain a parameter, if not and it contains the symbol $y$, so the other symbol is a bound variable, then only one such atomic subformula is allowed, if both variable symbols in an atomic subformula are bound then no more than one such atomic subformula is allowed and it must contain TWO distinct variables. – Zuhair Al-Johar Jun 6 '19 at 21:32