MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  ciun Unicode version

Syntax Definition ciun 4330
Description: Extend class notation to include indexed union. Note: Historically (prior to 21-Oct-2005), set.mm used the notation U.xe.A , with the same union symbol as cuni 4249. While that syntax was unambiguous, it did not allow for LALR parsing of the syntax constructions in set.mm. The new syntax uses a distinguished symbol U_ instead of U. and does allow LALR parsing. Thanks to Peter Backes for suggesting this change.
Hypotheses
Ref Expression
vx
cA
cB
Assertion
Ref Expression
ciun

See definition df-iun 4332 for more information.

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