Metamath Proof Explorer


Syntax definition cbc

Description: Extend class notation to include the binomial coefficient operation (combinatorial choose operation).

Ref Expression
Assertion cbc class C