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

Syntax Definition wbr 4452
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 9829.)
Hypotheses
Ref Expression
cA
cB
cR
Assertion
Ref Expression
wbr

See definition df-br 4453 for more information.

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