Metamath Proof Explorer

Metamath Proof Explorer

< Previous Next >
Related theorems
GIF version

Syntax Definition c0 1707

Description: Extend class notation to include the empty set.

**Assertion**
Ref	Expression
c0	class ∅

See definition df-nul 1708 for more information.

Colors of variables: wff set class