Metamath Proof Explorer


Theorem fzfid

Description: Commonly used special case of fzfi . (Contributed by Mario Carneiro, 25-May-2014)

Ref Expression
Assertion fzfid
|- ( ph -> ( M ... N ) e. Fin )

Proof

Step Hyp Ref Expression
1 fzfi
 |-  ( M ... N ) e. Fin
2 1 a1i
 |-  ( ph -> ( M ... N ) e. Fin )