Definition df-ndx

Description: Define the structure component index extractor. See Theorem ndxarg to understand its purpose. The restriction to NN ensures that ndx is a set. The restriction to some set is necessary since _I is a proper class. In principle, we could have chosen CC or (if we revise all structure component definitions such as df-base ) another set such as the set of finite ordinals _om ( df-om ). (Contributed by NM, 4-Sep-2011)

	Ref	Expression
Assertion	df-ndx	$$⊢\mathrm{ndx}={\mathrm{I}\upharpoonright }_{\mathbb{N}}$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cnx	$$class\mathrm{ndx}$$
1		cid	$$class\mathrm{I}$$
2		cn	$$class\mathbb{N}$$
3	1 2	cres	$$class\left({\mathrm{I}\upharpoonright }_{\mathbb{N}}\right)$$
4	0 3	wceq	$$wff\mathrm{ndx}={\mathrm{I}\upharpoonright }_{\mathbb{N}}$$