Metamath Proof Explorer


Syntax definition cdit

Description: Extend class notation with the directed integral.

Ref Expression
Assertion cdit class A B C dx