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

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

See definition df-iun 4124 for more information.

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