Metamath Proof Explorer


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 φ A Fin
ssfid.2 φ B A
Assertion ssfid φ B Fin

Proof

Step Hyp Ref Expression
1 ssfid.1 φ A Fin
2 ssfid.2 φ B A
3 ssfi A Fin B A B Fin
4 1 2 3 syl2anc φ B Fin