HomeHome Metamath Proof Explorer < Previous   Next >
Related theorems
Unicode version

Syntax Definition cfz 6467
Description: Extend class notation to include the notation for a contiguous finite set of integers. Read "M...N" as "the set of integers from M to N inclusive."
Assertion
Ref Expression
cfz class ...

See definition df-fz 6468 for more information.

Colors of variables: wff set class
Copyright terms: Public domain