Metamath Proof Explorer

Metamath Proof Explorer

< Previous Next >
Related theorems
GIF 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