Metamath Proof Explorer


Syntax definition csur

Description: Declare the class of all surreal numbers (see df-no ).

Ref Expression
Assertion csur class No