Metamath Proof Explorer


Syntax definition cund

Description: Extend class notation with undefined value function.

Ref Expression
Assertion cund
class Undef