Metamath Proof Explorer


Syntax definition cmin

Description: Extend class notation to include subtraction.

Ref Expression
Assertion cmin
class -