Metamath Proof Explorer 
< Previous
Next >
Nearby theorems 

Mirrors > Home > MPE Home > Th. List > co  Unicode version 
Description: Extend class notation to include the value of an operation (such as ) 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 9829.) 
Ref  Expression 

cA  
cB  
cF 
Ref  Expression 

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