HomeHome Metamath Proof Explorer < Previous   Next >
Related theorems
Unicode version
Syntax Definition cuz 6417
Description: Extend class notation with the upper integer function. Read "ZZ>` M" as "the set of integers greater than or equal to M."
Assertion
Ref Expression
cuz class ZZ>
See definition df-uz 6418 for more information.
Colors of variables: wff set class
Copyright terms: Public domain