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	|- ( A e. HF <-> ( A e. Fin /\ A C_ HF ) )

Proof

Step	Hyp	Ref	Expression
1		elhf4	|- ( A e. HF <-> ( A e. Fin /\ A. x e. A x e. HF ) )
2		dfss3	|- ( A C_ HF <-> A. x e. A x e. HF )
3	2	anbi2i	|- ( ( A e. Fin /\ A C_ HF ) <-> ( A e. Fin /\ A. x e. A x e. HF ) )
4	1 3	bitr4i	|- ( A e. HF <-> ( A e. Fin /\ A C_ HF ) )