Theorem hfelhf

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

	Ref	Expression
Assertion	hfelhf	Could not format assertion : No typesetting found for |- ( ( A e. B /\ B e. HF ) -> A e. HF ) with typecode |-

Proof

Step	Hyp	Ref	Expression
1		elhf4	Could not format ( B e. HF <-> ( B e. Fin /\ A. x e. B x e. HF ) ) : No typesetting found for |- ( B e. HF <-> ( B e. Fin /\ A. x e. B x e. HF ) ) with typecode |-
2	1	simprbi	Could not format ( B e. HF -> A. x e. B x e. HF ) : No typesetting found for |- ( B e. HF -> A. x e. B x e. HF ) with typecode |-
3		eleq1	Could not format ( x = A -> ( x e. HF <-> A e. HF ) ) : No typesetting found for |- ( x = A -> ( x e. HF <-> A e. HF ) ) with typecode |-
4	3	rspcva	Could not format ( ( A e. B /\ A. x e. B x e. HF ) -> A e. HF ) : No typesetting found for |- ( ( A e. B /\ A. x e. B x e. HF ) -> A e. HF ) with typecode |-
5	2 4	sylan2	Could not format ( ( A e. B /\ B e. HF ) -> A e. HF ) : No typesetting found for |- ( ( A e. B /\ B e. HF ) -> A e. HF ) with typecode |-