Metamath Proof Explorer 
< Previous
Next >
Nearby theorems 

Mirrors > Home > MPE Home > Th. List > ciun  Unicode version 
Description: Extend class notation to
include indexed union. Note: Historically
(prior to 21Oct2005), set.mm used the notation U. x e. 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. 
Ref  Expression 

vx  
cA  
cB 
Ref  Expression 

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