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	Could not format assertion : No typesetting found for |- ( A e. HF -> { A } e. HF ) with typecode |-

Proof

Step	Hyp	Ref	Expression
1		snfi	$$⊢\left\{A\right\}\in \mathrm{Fin}$$
2		snssi	Could not format ( A e. HF -> { A } C_ HF ) : No typesetting found for |- ( A e. HF -> { A } C_ HF ) with typecode |-
3		elhf3	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 |-
4	3	biimpri	Could not format ( ( { A } e. Fin /\ { A } C_ HF ) -> { A } e. HF ) : No typesetting found for |- ( ( { A } e. Fin /\ { A } C_ HF ) -> { A } e. HF ) with typecode |-
5	1 2 4	sylancr	Could not format ( A e. HF -> { A } e. HF ) : No typesetting found for |- ( A e. HF -> { A } e. HF ) with typecode |-