Metamath Proof Explorer


Syntax definition cz

Description: Extend class notation to include the class of integers.

Ref Expression
Assertion cz
class ZZ