Definition df-ndx 15860

Description: Define the structure component index extractor. See theorem ndxarg 15882 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 15863) another set such as the set of finite ordinals om (df-om 7066). (Contributed by NM, 4-Sep-2011.)

Assertion

Ref	Expression
df-ndx	|- ndx = ( _I |` NN )

Detailed syntax breakdown of Definition df-ndx

Step	Hyp	Ref	Expression
1		cnx 15854	. 2 class ndx
2		cid 5023	. . 3 class _I
3		cn 11020	. . 3 class NN
4	2, 3	cres 5116	. 2 class ( _I |` NN )
5	1, 4	wceq 1483	1 wff ndx = ( _I |` NN )

This definition is referenced by:  wunndx  15878  ndxarg  15882  bj-ndxarg  33029