Syntax Definition csu 6917

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

Hypotheses

Ref	Expression
cA	class A
cB	class B
vk	set k

Assertion

Ref	Expression
csu	class Σk ∈ A B

See definition df-sum 6918 for more information.

Copyright terms: Public domain