Let's work in [Quine's $\sf ML$][1], we can define classes after nonstratified formulas. Now for every set $X$ we can define the membership graph $\operatorname {MG}(X)$ on its transitive closure, that is the restriction of the graph of membership relation (which is a class) to the transitive closure class of $X$, so $$\operatorname {MG}(X)= E \cap  (\operatorname {trscl}(X) \times \operatorname {trscl}(X))$$; Where $E = \{(x,y) \mid x \in y, x \in V, y \in V\}$; 

$\operatorname {trscl}(X)=\{y \mid y=X \lor \forall T \,(trs(T) \land X \subseteq T \to y \in T) \}$


Now what I want to do is to instead of just stipulating Extensionality over $\sf SF$
(i.e.; [$\sf NF-Extensionality$][2]), we stipulate:

$$ \operatorname {MG}(X) \approx \operatorname {MG}(Y) \to X=Y.$$

where $(,)$ is defined after Wiener pairs; and $\approx$ stand for graph ismorphism.

I'd label this axiom as *Strong Extensionality*, and "Strong Extensionality + Stratified Comprehension" as *$\sf Strong \ NF$*.

Clearly Strong Extensionality proves Extensionality. But if we assume that $\sf NF$ is consistent, then would this be enough to prove the consistency of $\sf Strong \ NF$?

A related question is to adapt this to accommodate existence of Ur-elements, and ask the same question about consistency of $\sf Strong \ NFU$. In this case we require the ismorphisms in the axiom of Strong Extensionality to fix Ur-elements.


  [1]: https://books.google.iq/books?id=NJ7SBQAAQBAJ&pg=PA300&lpg=PA300&dq=Quines%20Mathematical%20logic%20ML%20free&source=bl&ots=z9mqRJgish&sig=ACfU3U2c029nQ6ec9w7eC4TW5i3L1hk89g&hl=en&sa=X&ved=2ahUKEwj_xImX_P_2AhVOtKQKHSBmANUQ6AF6BAgiEAM#v=onepage&q=Quines%20Mathematical%20logic%20ML%20free&f=false
  [2]: https://www.jstor.org/stable/2274915