Description: Define the empty set.
More precisely, we should write "empty class". It
will be posited in ax-nul 4983 that an empty set exists. Then, by
uniqueness
among classes (eq0 4130, as opposed to the weaker uniqueness among
sets,
nulmo 2791), it will follow that ∅ is indeed a set (0ex 4984).
Special
case of Exercise 4.10(o) of [Mendelson]
p. 231. For a more traditional
definition, but requiring a dummy variable, see dfnul2 4118. (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.) |