Intuitionistic Logic Explorer 
< Previous
Next >
Nearby theorems 

Mirrors > Home > ILE Home > Th. List > ciun  Structured version GIF version 
Description: Extend class notation to include indexed union. Note: Historically (prior to 21Oct2005), 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. 
Ref  Expression 

vx  setvar x 
cA  class A 
cB  class B 
Ref  Expression 

ciun  class ∪ x ∈ A B 
Colors of variables: wff set class 
Copyright terms: Public domain  W3C validator 