Description: Define the empty set. More precisely, we should write "empty class". It
will be posited in ax-nul that an empty set exists. Then, by uniqueness
among classes ( eq0 , as opposed to the weaker uniqueness among sets,
nulmo ), it will follow that (/) is indeed a set ( 0ex ). Special
case of Exercise 4.10(o) of Mendelson p. 231. For a more traditional
definition, but requiring a dummy variable, see dfnul2 . (Contributed by NM, 17-Jun-1993) Clarify that at this point, it is not established
that it is a set. (Revised by BJ, 22-Sep-2022)