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

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/. ~~ )

This definition is referenced by:  ncsex  6111  nulnnc  6118  elncs  6119