Metamath Proof Explorer


Syntax definition cdiv

Description: Extend class notation to include division.

Ref Expression
Assertion cdiv class /