NFE Home New Foundations Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  NFE Home  >  Th. List  >  df-0c Unicode 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
StepHypRef Expression
1 c0c 4374 . 2 0c
2 c0 3550 . . 3
32csn 3737 . 2
41, 3wceq 1642 1 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