Metamath Proof Explorer


Syntax definition cfn

Description: Extend class definition to include the class of all finite sets.

Ref Expression
Assertion cfn
class Fin