Let's work in Quine's $\sf ML$, 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$), 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.
