Syntax Definition ciun 1994

Description: Extend class notation to include indexed union.

Hypotheses

Ref	Expression
vx	set x
cA	class A
cB	class B

Assertion

Ref	Expression
ciun	class U.x e. A B

See definition df-iun 1996 for more information.

metamath.org