Syntax Definition csu 14416

Description: Extend class notation to include finite summations. (An underscore was added to the ASCII token in order to facilitate set.mm text searches, since "sum" is a commonly used word in comments.)

Hypotheses

Ref	Expression
cA	class A
cB	class B
vk	setvar k

Assertion

Ref	Expression
csu	class sum_ k e. A B

See definition df-sum 14417 for more information.