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