Definition df-ni

Description: Define the class of positive integers. This is a "temporary" set used in the construction of complex numbers df-c , and is intended to be used only by the construction. (Contributed by NM, 15-Aug-1995) (New usage is discouraged.)

	Ref	Expression
Assertion	df-ni	$$⊢𝑵=\mathrm{\omega }\setminus \left\{\varnothing \right\}$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cnpi	$$class𝑵$$
1		com	$$class\mathrm{\omega }$$
2		c0	$$class\varnothing$$
3	2	csn	$$class\left\{\varnothing \right\}$$
4	1 3	cdif	$$class\left(\mathrm{\omega }\setminus \left\{\varnothing \right\}\right)$$
5	0 4	wceq	$$wff𝑵=\mathrm{\omega }\setminus \left\{\varnothing \right\}$$