Metamath Proof Explorer


Syntax definition cestrc

Description: Extend class notation to include the category ExtStr.

Ref Expression
Assertion cestrc class ExtStrCat