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

Syntax Definition co 6129
 Description: Extend class notation to include the value of an operation (such as ?Error: + ^ This math symbol is not active (i.e. was not declared in this scope). ) for two arguments and . 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 9343.)
Hypotheses
Ref Expression
cA
cB
cF
Assertion
Ref Expression
co