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 ( 𝐸 ∈ Fin → ( 𝐸𝐵 ) ∈ Fin )

Proof

Step Hyp Ref Expression
1 resss ( 𝐸𝐵 ) ⊆ 𝐸
2 ssfi ( ( 𝐸 ∈ Fin ∧ ( 𝐸𝐵 ) ⊆ 𝐸 ) → ( 𝐸𝐵 ) ∈ Fin )
3 1 2 mpan2 ( 𝐸 ∈ Fin → ( 𝐸𝐵 ) ∈ Fin )