Metamath Proof Explorer


Syntax definition csec

Description: Extend class notation to include the secant function, see df-sec .

Ref Expression
Assertion csec
class sec