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	|- ( A e. HF -> { A } e. HF )

Proof

Step	Hyp	Ref	Expression
1		snfi	|- { A } e. Fin
2		snssi	|- ( A e. HF -> { A } C_ HF )
3		elhf3	|- ( { A } e. HF <-> ( { A } e. Fin /\ { A } C_ HF ) )
4	3	biimpri	|- ( ( { A } e. Fin /\ { A } C_ HF ) -> { A } e. HF )
5	1 2 4	sylancr	|- ( A e. HF -> { A } e. HF )