Is this theory consistent?
Language: first order language of set theory,
Extra-logical axioms:
1. Extensionality: as in $\sf NF$.
2. Stratified Comprehension: as in $\sf NF$.
Define: a set is said to be well founded if it is not an element of a descending membership set. Formally:
$$\operatorname {well-founded}(s) \iff \neg \exists x: s \in x \land \forall y \in x \exists z: z \in y \cap x $$
3. Replacement: if $A$ is a well founded set, and $\phi(x,y)$ is a formula standing for a many-to-one relation from well founded sets to well founded sets, that doesn't mention "$B$", then there is a set $B=\{y \mid \exists x \in A : \phi(x,y)\}$.
4. Infinity: There is a well-founded set having the empty set among its elements, that is closed under singletons.
5. Choice: For every nonempty set of pairwise disjoint well-founded nonempty sets, there is a set that has singleton intersections with each of its elements.
So, this theory has a universe obeying the rules of $\sf NF $, and has its well founded realm obeying the rules of $\sf ZFC$.
It is known that there is a consistent similar theory that extends $\sf NFU$. A corollary of Randall Holmes theory that speaks about the $\sf BEST$ model of $\sf NFU$. But, is this the case with $\sf NF$?
I've asked a similar question before but in terms of $\sf ML$, this question is in terms of $\sf NF$.
