New Foundations Explorer		< Previous   Next > Nearby theorems
Mirrors  >  Home  >  NFE Home  >  Th. List  >  df-0c		GIF version

---

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 = {∅}

Colors of variables: wff setvar class

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

Copyright terms: Public domain

W3C validator