Metamath Proof Explorer


Syntax definition cxad

Description: Extend class notation to include addition of extended reals.

Ref Expression
Assertion cxad
class +e