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

Syntax Definition csup 7920
Description: Extend class notation to include supremum of class . Here is ordinarily a relation that strictly orders class . For example, could be 'less than' and could be the set of real numbers.
Hypotheses
Ref Expression
cA
cB
cR
Assertion
Ref Expression
csup

See definition df-sup 7921 for more information.

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