Theorem ssfid

Description: A subset of a finite set is finite, deduction version of ssfi . (Contributed by Glauco Siliprandi, 21-Nov-2020)

	Ref	Expression
Hypotheses	ssfid.1	$$⊢\phi \to A\in \mathrm{Fin}$$
	ssfid.2	$$⊢\phi \to B\subseteq A$$
Assertion	ssfid	$$⊢\phi \to B\in \mathrm{Fin}$$

Proof

Step	Hyp	Ref	Expression
1		ssfid.1	$$⊢\phi \to A\in \mathrm{Fin}$$
2		ssfid.2	$$⊢\phi \to B\subseteq A$$
3		ssfi	$$⊢\left(A\in \mathrm{Fin}\wedge B\subseteq A\right)\to B\in \mathrm{Fin}$$
4	1 2 3	syl2anc	$$⊢\phi \to B\in \mathrm{Fin}$$