Metamath Proof Explorer


Syntax definition cxdiv

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

Ref Expression
Assertion cxdiv class ÷ 𝑒