Metamath Proof Explorer


Syntax definition cp0

Description: Extend class notation with poset zero.

Ref Expression
Assertion cp0 class 0.