Metamath Proof Explorer


Syntax definition ccnf

Description: Extend class notation with the Cantor normal form function.

Ref Expression
Assertion ccnf class CNF