Metamath Proof Explorer


Syntax definition ccom

Description: Extend the definition of a class to include the composition of two classes. (Read: The composition of A and B .)

Ref Expression
Assertion ccom class A B