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	⊢ ∅
1		cvv	⊢ V
2	1 1	cdif	⊢ ( V ∖ V )
3	0 2	wceq	⊢ ∅ = ( V ∖ V )