Definition df-on 4404

Description: Define the class of all ordinal numbers. Definition 7.11 of [TakeutiZaring] p. 38. (Contributed by NM, 5-Jun-1994.)

Assertion

Ref	Expression
df-on	|- On = { x | Ord x }

Detailed syntax breakdown of Definition df-on

Step	Hyp	Ref	Expression
1		con0 4399	. 2 class On
2		vx	. . . . 5 setvar x
3	2	cv 1363	. . . 4 class x
4	3	word 4398	. . 3 wff Ord x
5	4, 2	cab 2182	. 2 class { x | Ord x }
6	1, 5	wceq 1364	1 wff On = { x | Ord x }

This definition is referenced by:  elong  4409  ordon  4523