Metamath Proof Explorer

Syntax definition c0

Description: Extend class notation to include the empty set.

Ref Expression
Assertion c0 
class (/)