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	$$⊢\varnothing =\mathrm{V}\setminus \mathrm{V}$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		c0	$$class\varnothing$$
1		cvv	$$class\mathrm{V}$$
2	1 1	cdif	$$class\left(\mathrm{V}\setminus \mathrm{V}\right)$$
3	0 2	wceq	$$wff\varnothing =\mathrm{V}\setminus \mathrm{V}$$