New Foundations Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > NFE Home > Th. List > df-ncs | GIF version |
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.) |
Ref | Expression |
---|---|
df-ncs | ⊢ NC = (V / ≈ ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | cncs 6088 | . 2 class NC | |
2 | cvv 2859 | . . 3 class V | |
3 | cen 6028 | . . 3 class ≈ | |
4 | 2, 3 | cqs 5946 | . 2 class (V / ≈ ) |
5 | 1, 4 | wceq 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 |