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	⊢ ( 𝐴 ∈ HF ↔ ( 𝐴 ∈ Fin ∧ 𝐴 ⊆ HF ) )

Proof

Step	Hyp	Ref	Expression
1		elhf4	⊢ ( 𝐴 ∈ HF ↔ ( 𝐴 ∈ Fin ∧ ∀ 𝑥 ∈ 𝐴 𝑥 ∈ HF ) )
2		dfss3	⊢ ( 𝐴 ⊆ HF ↔ ∀ 𝑥 ∈ 𝐴 𝑥 ∈ HF )
3	2	anbi2i	⊢ ( ( 𝐴 ∈ Fin ∧ 𝐴 ⊆ HF ) ↔ ( 𝐴 ∈ Fin ∧ ∀ 𝑥 ∈ 𝐴 𝑥 ∈ HF ) )
4	1 3	bitr4i	⊢ ( 𝐴 ∈ HF ↔ ( 𝐴 ∈ Fin ∧ 𝐴 ⊆ HF ) )