Definition df-on 6366

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 = {𝑥 ∣ Ord 𝑥}

Detailed syntax breakdown of Definition df-on

Step	Hyp	Ref	Expression
1		con0 6362	. 2 class On
2		vx	. . . . 5 setvar 𝑥
3	2	cv 1568	. . . 4 class 𝑥
4	3	word 6361	. . 3 wff Ord 𝑥
5	4, 2	cab 2738	. 2 class {𝑥 ∣ Ord 𝑥}
6	1, 5	wceq 1569	1 wff On = {𝑥 ∣ Ord 𝑥}

This definition is used by:  elong  6370  onprcr  36548  onprcALT  36549  dfon2  36646