Metamath Proof Explorer

Syntax definition cund

Description: Extend class notation with undefined value function.

Ref Expression
Assertion cund 
class Undef