We introduce a new symbol $\lambda$ to denote class-abstractions, and we add the following rule:

if $\phi$ is a formula that use $``\mu"$, and in which the symbol $\sf y$ doesn't occur; then: $\lambda \phi \text { is a term}$.

$\mu$ is a contant symbol.

We stipulate that every $\lambda$-term is not quantified upon, so $``\forall \lambda \phi,\exists \lambda \phi"$ are not parts of formulas of our language. However, they can seep into the quantifiers indirectly if we have them equal to some non-$\lambda$-term, so if we have $\exists x: \lambda \phi=x$ then this $\lambda$-term would be quantified upon implicitly within $\forall s, \exists s$

The expression $\phi^{\sf y}$ means the formula obtained from a formula $\phi$ where $\lambda \phi$ is a term, by merely replacing all occurrences of the symbol $\mu$ by the symbol ${\sf y}$.

Axioms:

Extensionality: $ \forall \vec{w} : \forall {\sf y} (\phi^{\sf y} \leftrightarrow \psi^{\sf y}) \iff\lambda \phi = \lambda \psi $

Comprehension: $\forall \vec{w}: \forall {\sf y} ({\sf y} \in \lambda \phi \iff \phi^{\sf y})$

$\sf Define:$ $set\,\lambda \phi \iff \exists s: s =\lambda \phi$

ٌRepresentation: $ \forall a: a= \lambda (\mu \in a)$

Membership: $ \forall \vec{w} : (\lambda \phi \in \lambda \psi) \to set \, \lambda \phi$

Separation: $ \forall \vec{w} \forall a: set\,\lambda (\mu \in a \land \phi)$

Replacement: $ \forall \vec{w} \forall a: set \,\lambda (\exists x \in a \forall z (\psi(x,z) \leftrightarrow z=\mu))$

We write the rest of axioms of ZF in $\lambda$-terms as:

Pairing: $\forall a \forall b: set \, \lambda (\mu = a \lor \mu = b)$

Union: $\forall a: set \, \lambda (\exists x \in a: \mu \in x)$

Power: $\forall a: set \, \lambda (\mu \subseteq a)$

Infinity: $set \, \lambda (\mu \text{ is a finite ordinal})$

Foundation: $\forall \vec{w} : \exists x \in \lambda \phi \to \exists x \in \lambda \phi \, \forall y \in \lambda \phi \, (y \not \in x)$

To express global choice we need to add a primitive binary relation symbol $\in^* $, denoting "is chosen from", then axiomatize:

$\forall x: \forall y \in^* x \, (y \in x) \land [x \neq \emptyset \to \exists! y: y \in^* x] $

So for any set $A$, the set of all chosen elements from elements of $A$ is $\lambda (\exists x \in A : \mu \in^* x)$.

Also we can have this actually for any class $\lambda \phi$, so we have $\lambda (\exists x \in \lambda \phi : \mu \in^* x)$ being the choice class of any class $\lambda \phi$

I'm introducing this notation, but at the same time I have a question about the above system. I wonder if it is equi-consistent with NBG? The idea here is that all classes (i.e., $\lambda$-terms) that are not sets won't be quantified upon, simply the language here is restricting them from being so. So I think that this restriction would inherently render class comprehension equivalent to that of NBG.

However, generally speaking the language of NBG seems to be stronger than this one. The reason is because it does have class variables that are quantified upon!

I think that NBG theorems about proper classes are not expressible here. Also this system might not be finitely axiomatizable? Hence my question:

Can NBG be interpreted in this system?

Is there a problem in the notation used in this system?