Metamath Proof Explorer


Syntax definition cc0

Description: Extend class notation to include the complex number 0.

Ref Expression
Assertion cc0
class 0