Metamath Proof Explorer


Syntax definition chfstruct

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

Ref Expression
Assertion chfstruct Could not format assertion : No typesetting found for class HFStruct with typecode class