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

Syntax Definition co 6073
Description: Extend class notation to include the value of an operation 
F (such as  +) for two arguments  A and  B. Note that the syntax is simply three class symbols in a row surrounded by parentheses. Since operation values are the only possible class expressions consisting of three class expressions in a row surrounded by parentheses, the syntax is unambiguous. (For an example of how syntax could become ambiguous if we are not careful, see the comment in cneg 9284.)
Hypotheses
Ref Expression
cA  class  A
cB  class  B
cF  class  F
Assertion
Ref Expression
co  class  ( A F B )

See definition df-ov 6076 for more information.

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