This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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	$⊢ \emptyset = V ∖ V$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		c0	$class \emptyset$
1		cvv	$class V$
2	1 1	cdif	$class (V ∖ V)$
3	0 2	wceq	$wff \emptyset = V ∖ V$