Metamath Proof Explorer


Syntax definition cfa

Description: Extend class notation to include the factorial of nonnegative integers.

Ref Expression
Assertion cfa class !