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	$$⊢\mathrm{On}=\left\{x|\mathrm{Ord}x\right\}$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		con0	$$class\mathrm{On}$$
1		vx	$$setvarx$$
2	1	cv	$$setvarx$$
3	2	word	$$wff\mathrm{Ord}x$$
4	3 1	cab	$$class\left\{x|\mathrm{Ord}x\right\}$$
5	0 4	wceq	$$wff\mathrm{On}=\left\{x|\mathrm{Ord}x\right\}$$