Database
SUPPLEMENTARY MATERIAL (USERS' MATHBOXES)
Mathbox for Scott Fenton
Hereditarily Finite Sets
chf
Next ⟩
df-hf
Metamath Proof Explorer
Unicode
Structured
Syntax definition
chf
Description:
The constant
Hf
is a class.
Ref
Expression
Assertion
chf
class Hf