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 )