Theorem elhf3

Description: A set is hereditarily finite if and only if it is finite and all its members are hereditarily finite. (Contributed by Eric Schmidt, 8-Sep-2026) Avoid ax-reg , ax-inf2 . (Revised by BTernaryTau, 17-Sep-2026)

	Ref	Expression
Assertion	elhf3	Could not format assertion : No typesetting found for |- ( A e. HF <-> ( A e. Fin /\ A C_ HF ) ) with typecode |-

Proof

Step	Hyp	Ref	Expression
1		elhf4	Could not format ( A e. HF <-> ( A e. Fin /\ A. x e. A x e. HF ) ) : No typesetting found for |- ( A e. HF <-> ( A e. Fin /\ A. x e. A x e. HF ) ) with typecode |-
2		dfss3	Could not format ( A C_ HF <-> A. x e. A x e. HF ) : No typesetting found for |- ( A C_ HF <-> A. x e. A x e. HF ) with typecode |-
3	2	anbi2i	Could not format ( ( A e. Fin /\ A C_ HF ) <-> ( A e. Fin /\ A. x e. A x e. HF ) ) : No typesetting found for |- ( ( A e. Fin /\ A C_ HF ) <-> ( A e. Fin /\ A. x e. A x e. HF ) ) with typecode |-
4	1 3	bitr4i	Could not format ( A e. HF <-> ( A e. Fin /\ A C_ HF ) ) : No typesetting found for |- ( A e. HF <-> ( A e. Fin /\ A C_ HF ) ) with typecode |-