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

Definition df-nc 6101
Description: Define the cardinality operation. This is the unique cardinal number containing a given set. Definition from [Rosser] p. 371. (Contributed by Scott Fenton, 24-Feb-2015.)
Assertion
Ref Expression
df-nc Nc A = [A] ≈

Detailed syntax breakdown of Definition df-nc
StepHypRef Expression
1 cA . . 3 class A
21cnc 6091 . 2 class Nc A
3 cen 6028 . . 3 class
41, 3cec 5945 . 2 class [A] ≈
52, 4wceq 1642 1 wff Nc A = [A] ≈
Colors of variables: wff setvar class
This definition is referenced by:  nceq  6108  ncex  6117  elncs  6119  ncidg  6122  ncprc  6124  elnc  6125  eqncg  6126  ncseqnc  6128  mucnc  6131  df0c2  6137  1cnc  6139  ncdisjeq  6148
  Copyright terms: Public domain W3C validator