Metamath Proof Explorer


Syntax definition ccrd

Description: Extend class definition to include the cardinal size function.

Ref Expression
Assertion ccrd class card