MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  ciin Structured version   Visualization version   GIF version

Syntax Definition ciin 4913
Description: Extend class notation to include indexed intersection. Note: Historically (prior to 21-Oct-2005), set.mm used the notation 𝑥𝐴𝐵, with the same intersection symbol as cint 4869. Although 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 instead of and does allow LALR parsing. Thanks to Peter Backes for suggesting this change.
Hypotheses
Ref Expression
vx setvar 𝑥
cA class 𝐴
cB class 𝐵
Assertion
Ref Expression
ciin class 𝑥𝐴 𝐵

See definition df-iin 4915 for more information.

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