Theorem hfsn

Description: The singleton of a hereditarily finite set is a hereditarily finite set. (Contributed by Scott Fenton, 15-Jul-2015) Avoid ax-reg , ax-inf2 . (Revised by BTernaryTau, 17-Sep-2026)

	Ref	Expression
Assertion	hfsn	⊢ ( 𝐴 ∈ HF → { 𝐴 } ∈ HF )

Proof

Step	Hyp	Ref	Expression
1		snfi	⊢ { 𝐴 } ∈ Fin
2		snssi	⊢ ( 𝐴 ∈ HF → { 𝐴 } ⊆ HF )
3		elhf3	⊢ ( { 𝐴 } ∈ HF ↔ ( { 𝐴 } ∈ Fin ∧ { 𝐴 } ⊆ HF ) )
4	3	biimpri	⊢ ( ( { 𝐴 } ∈ Fin ∧ { 𝐴 } ⊆ HF ) → { 𝐴 } ∈ HF )
5	1 2 4	sylancr	⊢ ( 𝐴 ∈ HF → { 𝐴 } ∈ HF )