Working in $\sf ML$$\sf U$:
Define: $x \in^f y \iff f(x) \in y$
by $\varphi^f$ we mean the formula obtained by merely replacing each "$\in$" symbol in formula $\varphi$ by the symbol "$\in^f$".
Symmetric Comprehension: Let $\phi$ be the formula "$\forall y \, (y \in x \leftrightarrow y \in V \land \varphi(y,a,b))$" where $\varphi(y,a,b)$ is a formula whose free variables are "$y,a,b$", and whose quantifiers are all bounded by $V$. Then:
$\forall a \in V \forall b \in V \forall x: \\ \phi \land \forall f\, ( \operatorname {auto}(f) \land f(a)=a \land f(b)=b \to (\phi \leftrightarrow \phi^f)) \\ \to x \in V$
In English: if a definable class has a definition that is preserved under all automorphisms of the class of all sets that fix all its parameters, then this class is a set.
Where automorphism is defined in the usual manner as a bijection from $V$ to $V$ that preserves $\in$ membership over $V$. That is:
$\begin{align} \operatorname {auto}(f) \iff & (f: V \to V) \ \land \\ & f \text { is a bijection} \ \land \\ & \forall x \in V \forall y \in V \, (x \in y \leftrightarrow f(x) \in f(y)) \end{align} $
Is symmetric comprehension provable in $\sf MLU$?
To be noticed is that Symmetric comprehension extending Weak Extensionality, Class Comprehension schema (of $\sf MK$) and Pairing (any class having no more than two elements, is a set), does prove all axioms of $\sf MLU$. The point actually is if $\sf MLU$ is equivalent to this simplified version of symmetric class theory.
