This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem fzfid

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

		Ref	Expression
	Assertion	fzfid	$⊢ φ \to (M \dots N) \in Fin$

Step	Hyp	Ref	Expression
1		fzfi	$⊢ (M \dots N) \in Fin$
2	1	a1i	$⊢ φ \to (M \dots N) \in Fin$