Database
ZF (ZERMELO-FRAENKEL) SET THEORY
ZF Set Theory - add the Axiom of Union
Hartogs function
char

Next ⟩ df-har

Metamath Proof Explorer

Unicode
Structured

Syntax definition char

Description: Class symbol for the Hartogs function.

		Ref	Expression
	Assertion	char	class har