Definition df-0c 4377

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 4374	. 2 class 0c
2		c0 3550	. . 3 class (/)
3	2	csn 3737	. 2 class {(/)}
4	1, 3	wceq 1642	1 wff 0c = {(/)}

This definition is referenced by:  0cex  4392  0cnsuc  4401  addcid1  4405  el0c  4421  nnsucelr  4428  nndisjeq  4429  ssfin  4470  0ceven  4505  lec0cg  6198