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 
|- ( ph -> A e. Fin )
ssfid.2 
|- ( ph -> B C_ A )
Assertion ssfid 
|- ( ph -> B e. Fin )

Proof

Step Hyp Ref Expression
1 ssfid.1 
 |-  ( ph -> A e. Fin )
2 ssfid.2 
 |-  ( ph -> B C_ A )
3 ssfi 
 |-  ( ( A e. Fin /\ B C_ A ) -> B e. Fin )
4 1 2 3 syl2anc 
 |-  ( ph -> B e. Fin )