Metamath Proof Explorer


Syntax definition cust

Description: Extend class notation with the class function of uniform structures.

Ref Expression
Assertion cust class UnifOn