Syntax Definition ccdn 3711

Description: Extend class definition to include the class of all cardinal numbers.

Assertion

Ref	Expression
ccdn	class Card

See definition df-cardn 3712 for more information.

metamath.org