ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  ciun Structured version   GIF version

Syntax Definition ciun 3627
Description: Extend class notation to include indexed union. Note: Historically (prior to 21-Oct-2005), set.mm used the notation x AB, with the same union symbol as cuni 3550. 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 instead of and does allow LALR parsing. Thanks to Peter Backes for suggesting this change.
Hypotheses
Ref Expression
vx setvar x
cA class A
cB class B
Assertion
Ref Expression
ciun class x A B

See definition df-iun 3629 for more information.

Colors of variables: wff set class
  Copyright terms: Public domain W3C validator