Syntax Definition coa 3101

Description: Extend the definition of a class to include the ordinal addition operation.

Assertion

Ref	Expression
coa	class +o

See definition df-oadd 3106 for more information.

metamath.org