Empty set in Morse-Kelley set theory Is it possible to prove the existence of the empty set in MK without the axiom schema of class comprehension (ASoCC)?
My conjecture is: No. Either one postulates the existence or proves it via the ASoCC.
Furthermore, the proof I came up with (using AsoCC) does only guarantee $\emptyset$ to be a class but not necessarliy a set. How could I prove that $\emptyset$ is infact no proper class? 
Thank you in advance!
Proposition (Existence of $\eta$)
There exists a class $\eta$ that does not contain any elements. 
$$ \exists \eta ~ (\forall a ~ \neg (a \in \eta)) ~~.$$
Proof:
Let $a$ be a set and assume the predicate $\psi(a) :\Leftrightarrow \neg (a = a)$, and $\eta$ such that
$$ \forall (a \in \eta \Leftrightarrow \psi (a)) ~~. $$
The existence of $\eta$ is guaranteed by the Axiom Schema of Class Comprehension and, by proposition ($\forall a (a=a)$), it has in fact the desired property that $(\forall a ~ \neg (a \in \eta))$.
 A: That depends on exactly how the other axioms are formulated, which not not something there's a strong consensus between authors about.
For example, as noted in the comments the axiom of infinity is supposed to guarantee that the inductive set it gives us ontains the empty set. But will that be phrased as
$$ \exists a( \forall n(\forall z(z\notin n) \to n\in a) \land \cdots ) $$
or
$$ \exists a( \exists n(\forall z(z\notin n) \land n\in a) \land \cdots )? $$
In the presence of the other axioms of the full system, these two are equivalent, so there is usually no need to care about which of them is the actual axiom of infinity.

Authors who care in particular about studying the consequences of subsets of the theory will tend to have an explicit axiom saying up front that an empty set exists, so you can cut away the infinity and comprehension axioms and still have something that behaves interestingly.
On the other hand, authors who care more about ease of arguing that such-and-such set or class is a model for the theory will want to make the axioms as simple and bare-bones and possible, to save work. They will be happy to let the axiom of infinity be our only guarantee that there even are any sets, and then use comprehension to create an empty set afterwards.
Each of these conflicting considerations can be said to be in the name of elegance, for a particular purpose.
