Metamath Proof Explorer

Definition df-nul

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)

Ref Expression
Assertion df-nul = V V

Detailed syntax breakdown

Step Hyp Ref Expression
0 c0 class
1 cvv class V
2 1 1 cdif class V V
3 0 2 wceq wff = V V