Definition df-ndx 16745

Description: Define the structure component index extractor. See Theorem ndxarg 16747 to understand its purpose. The restriction to ℕ 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 ℂ or (if we revise all structure component definitions such as df-base 16761) another set such as the set of finite ordinals ω (df-om 7645). (Contributed by NM, 4-Sep-2011.)

Assertion

Ref	Expression
df-ndx	⊢ ndx = ( I ↾ ℕ)

Detailed syntax breakdown of Definition df-ndx

Step	Hyp	Ref	Expression
1		cnx 16744	. 2 class ndx
2		cid 5454	. . 3 class I
3		cn 11830	. . 3 class ℕ
4	2, 3	cres 5553	. 2 class ( I ↾ ℕ)
5	1, 4	wceq 1543	1 wff ndx = ( I ↾ ℕ)

This definition is referenced by:  wunndx  16746  ndxarg  16747  bj-ndxarg  34983