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

Definition df-ncs 6098
Description: Define the set of all cardinal numbers. We define them as equivalence classes of sets of the same size. Definition from [Rosser] p. 372. (Contributed by Scott Fenton, 24-Feb-2015.)
Assertion
Ref Expression
df-ncs NC = (V / ≈ )

Detailed syntax breakdown of Definition df-ncs
StepHypRef Expression
1 cncs 6088 . 2 class NC
2 cvv 2859 . . 3 class V
3 cen 6028 . . 3 class
42, 3cqs 5946 . 2 class (V / ≈ )
51, 4wceq 1642 1 wff NC = (V / ≈ )
Colors of variables: wff setvar class
This definition is referenced by:  ncsex  6111  nulnnc  6118  elncs  6119
  Copyright terms: Public domain W3C validator