Metamath Proof Explorer


Syntax definition chfstruct

Description: Extend class notation with the set of structures whose components are hereditarily finite.

Ref Expression
Assertion chfstruct
class HFStruct