Metamath Proof Explorer


Syntax definition cida

Description: Extend class notation to include identity for arrows.

Ref Expression
Assertion cida class Ida