Definition df-0c 4378

Description: Define cardinal zero. (Contributed by SF, 12-Jan-2015.)

Assertion

Ref	Expression
df-0c	⊢ 0c = {∅}

Detailed syntax breakdown of Definition df-0c

Step	Hyp	Ref	Expression
1		c0c 4375	. 2 class 0c
2		c0 3551	. . 3 class ∅
3	2	csn 3738	. 2 class {∅}
4	1, 3	wceq 1642	1 wff 0c = {∅}

This definition is referenced by:  0cex  4393  0cnsuc  4402  addcid1  4406  el0c  4422  nnsucelr  4429  nndisjeq  4430  ssfin  4471  0ceven  4506  lec0cg  6199