Definition df-on 3847

Description: Define the class of all ordinal numbers. Definition 7.11 of [TakeutiZaring] p. 38.

Assertion

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

Detailed syntax breakdown of Definition df-on

Step	Hyp	Ref	Expression
1		con0 3843	. 2 class On
2		vx	. . . . 5 set x
3	2	cv 1614	. . . 4 class x
4	3	word 3842	. . 3 wff Ord x
5	4, 2	cab 2157	. 2 class {x | Ord x}
6	1, 5	wceq 1615	1 wff On = {x | Ord x}

This definition is referenced by:  elong 3851  dfon2 14739  dfom5b 15020

Copyright terms: Public domain