Syntax Definition ciun 2566

Description: Extend class notation to include indexed union. Note: Historically (prior to 21-Oct-2005), set.mm used the notation U.x e. AB, with the same union symbol as cuni 2503. While that syntax was unambiguous, it did not allow for LALR parsing of the syntax constructions in set.mm. The new syntax uses as distinguished symbol U_ instead of U. and does allow LALR parsing. Thanks to Peter Backes for suggesting this change.

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 2568 for more information.

Copyright terms: Public domain