Syntax Definition com 2372

Description: Extend class notation to include the class of natural numbers.

Assertion

Ref	Expression
com	class ω

See definition df-om 2373 for more information.

metamath.org