Metamath Proof Explorer


Syntax definition chf

Description: The constant Hf is a class.

Ref Expression
Assertion chf class Hf