This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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\}$

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