Slight Reformulation of ASC

This is a slightly different formulation of the theory of classes and atoms, $\mathsf{ASC}$ ("atoms, sets and classes") that I rather like, because of its generality (it permits urelemente/atoms and has impredicative comprehension) and its minimal restrictions. It is closely related to $\mathsf{MKA}$, Morse-Kelley class theory with atoms.

The official language $L$ of $\mathsf{ASC}$ is a 1-sorted first-order language, with variables

$X,Y, Z, X_1, X_2, \dots$ 

and three primitive predicates:

$X = Y$ for "$X$ is identical to $Y$"
$X \in Y$ for "$X$ is an element of $Y$"
$\mathsf{Class}(X)$ for "$X$ is a class"

We introduce explicit definitions:

$\mathsf{Memb}(X)$ is short for $\exists Y(X \in Y)$.
$\mathsf{Set}(X)$ is short for $\mathsf{Class}(X) \wedge \mathsf{Memb}(X)$.
$\mathsf{Atom}(X)$ is short for $\neg \mathsf{Class}(X) \wedge \mathsf{Memb}(X)$.
$X \equiv Y$ is short for $\forall Z(Z \in X \leftrightarrow Z \in Y)$.

In quantifiers, it's convenient to use somewhat type-theoretic looking abbreviations:

$X : \mathsf{Class}$ for $\mathsf{Class}(X)$.
$X : \mathsf{Memb}$ for $\mathsf{Memb}(X)$.
$X : \mathsf{Atom}$ for $\mathsf{Atom}(X)$.

For quantification over members, one may introduce a new variable sort $x,y,z, \dots$ as follows:

$\forall x \phi(x)$ is short for $(\forall X : \mathsf{Memb}) \phi(X))$

Then the axioms look a bit prettier:

Axioms of $\mathsf{ASC}$:
(COMP) $\hspace{10mm}$ $(\exists X: \mathsf{Class})\forall y(y \in X \leftrightarrow \phi(y)).$
(EXT) $\hspace{13mm}$ $(\forall X : \mathsf{Class})(\forall Y : \mathsf{Class})
(X \equiv Y \to X = Y).$
(ATOM) $\hspace{10mm}$ $(\forall X: \mathsf{Atom})\forall Y(Y \notin X).$

These are impredicative class comprehension (restricted to members), extensionality (restricted to classes) and an axiom saying that atoms are empty. One may write down any formula $\phi(y)$ for comprehension (with $X$ not free of course!). Consistency of comprehension (COMP) is ensured because the inner quantification only goes over members.

As mentioned before, this "second-order" theory $\mathsf{ASC}$ of classes is very weak. It has 1-element models. More generally, the models are related to power-set Boolean algebras, analogous to how models for $\mathsf{MK}$ can be understood as $\mathcal{P}(V_{\alpha})$, with $\alpha$ inaccessible.