Database
ZF (ZERMELO-FRAENKEL) SET THEORY
ZF Set Theory - add the Axiom of Infinity
Hereditarily finite sets
chf
Next ⟩
df-hf
Metamath Proof Explorer
Ascii
Unicode
Syntax definition
chf
Description:
Extend class notation with the class of hereditarily finite sets.
Ref
Expression
Assertion
chf
Could not format assertion : No typesetting found for class HF with typecode class