Syntax Definition ccda 3714

Description: Extend class definition to include cardinal number addition.

Assertion

Ref	Expression
ccda	class +c

See definition df-cda 3715 for more information.

metamath.org