Metamath Proof Explorer

Syntax definition zring

Description: Extend class notation with the (unital) ring of integers.

Ref Expression
Assertion zring 
class ZZring