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

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		con0	⊢ On
1		vx	⊢ 𝑥
2	1	cv	⊢ 𝑥
3	2	word	⊢ Ord 𝑥
4	3 1	cab	⊢ { 𝑥 ∣ Ord 𝑥 }
5	0 4	wceq	⊢ On = { 𝑥 ∣ Ord 𝑥 }