Metamath Proof Explorer 
< Previous
Next >
Nearby theorems 

Mirrors > Home > MPE Home > Th. List > wbr  Structured version Unicode version 
Description: Extend wff notation to include the general binary relation predicate. Note that the syntax is simply three class symbols in a row. Since binary relations are the only possible wff expressions consisting of three class expressions in a row, the syntax is unambiguous. (For an example of how syntax could become ambiguous if we are not careful, see the comment in cneg 9719.) 
Ref  Expression 

cA  
cB  
cR 
Ref  Expression 

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