Metamath Proof Explorer

Definition df-on

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

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

Detailed syntax breakdown

Step Hyp Ref Expression
0 con0 
 |-  On
1 vx 
 |-  x
2 1 cv 
 |-  x
3 2 word 
 |-  Ord x
4 3 1 cab 
 |-  { x | Ord x }
5 0 4 wceq 
 |-  On = { x | Ord x }