Theorem hfsshf

Description: Any subset of a hereditarily finite set is itself a hereditarily finite set. (Contributed by BTernaryTau, 17-Sep-2026)

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

Proof

Step	Hyp	Ref	Expression
1		hffi	Could not format ( B e. HF -> B e. Fin ) : No typesetting found for |- ( B e. HF -> B e. Fin ) with typecode |-
2		ssfi	$$⊢\left(B\in \mathrm{Fin}\wedge A\subseteq B\right)\to A\in \mathrm{Fin}$$
3	2	ancoms	$$⊢\left(A\subseteq B\wedge B\in \mathrm{Fin}\right)\to A\in \mathrm{Fin}$$
4	1 3	sylan2	Could not format ( ( A C_ B /\ B e. HF ) -> A e. Fin ) : No typesetting found for |- ( ( A C_ B /\ B e. HF ) -> A e. Fin ) with typecode |-
5		elhf3	Could not format ( B e. HF <-> ( B e. Fin /\ B C_ HF ) ) : No typesetting found for |- ( B e. HF <-> ( B e. Fin /\ B C_ HF ) ) with typecode |-
6	5	simprbi	Could not format ( B e. HF -> B C_ HF ) : No typesetting found for |- ( B e. HF -> B C_ HF ) with typecode |-
7		sstr	Could not format ( ( A C_ B /\ B C_ HF ) -> A C_ HF ) : No typesetting found for |- ( ( A C_ B /\ B C_ HF ) -> A C_ HF ) with typecode |-
8	6 7	sylan2	Could not format ( ( A C_ B /\ B e. HF ) -> A C_ HF ) : No typesetting found for |- ( ( A C_ B /\ B e. HF ) -> A C_ HF ) with typecode |-
9		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 |-
10	4 8 9	sylanbrc	Could not format ( ( A C_ B /\ B e. HF ) -> A e. HF ) : No typesetting found for |- ( ( A C_ B /\ B e. HF ) -> A e. HF ) with typecode |-