Metamath Proof Explorer


Syntax definition cida

Description: Extend class notation to include identity for arrows.

Ref Expression
Assertion cida
class IdA