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?