Syntax Definition ccrd 3620

Description: Extend class definition to include the cardinal size function.

Assertion

Ref	Expression
ccrd	class card

See definition df-card 3623 for more information.

metamath.org