HomeHome Metamath Proof Explorer < Previous   Next >
Related theorems
Unicode version
Syntax Definition cc0 4028
Description: Extend class notation to include the complex number 0.
Assertion
Ref Expression
cc0 class 0
See definition df-0 4035 for more information.
Colors of variables: wff set class
metamath.org