Definition df-ncs 6099

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

Step	Hyp	Ref	Expression
1		cncs 6089	. 2 class NC
2		cvv 2860	. . 3 class _V
3		cen 6029	. . 3 class ~~
4	2, 3	cqs 5947	. 2 class (_V/. ~~ )
5	1, 4	wceq 1642	1 wff NC = (_V/. ~~ )

This definition is referenced by:  ncsex  6112  nulnnc  6119  elncs  6120