Metamath Proof Explorer

Theorem finresfin

Description: The restriction of a finite set is finite. (Contributed by Alexander van der Vekens, 3-Jan-2018)

Ref Expression
Assertion finresfin ⊢E∈Fin→E↾B∈Fin

Proof

Step Hyp Ref Expression
1 resss ⊢E↾B⊆E
2 ssfi ⊢E∈Fin∧E↾B⊆E→E↾B∈Fin
3 1 2 mpan2 ⊢E∈Fin→E↾B∈Fin