Theorem fz1sbc

Description: Quantification over a one-member finite set of sequential integers in terms of substitution. (Contributed by NM, 28-Nov-2005)

	Ref	Expression
Assertion	fz1sbc	|- ( N e. ZZ -> ( A. k e. ( N ... N ) ph <-> [. N / k ]. ph ) )

Proof

Step	Hyp	Ref	Expression
1		sbc6g	|- ( N e. ZZ -> ( [. N / k ]. ph <-> A. k ( k = N -> ph ) ) )
2		df-ral	|- ( A. k e. ( N ... N ) ph <-> A. k ( k e. ( N ... N ) -> ph ) )
3		elfz1eq	|- ( k e. ( N ... N ) -> k = N )
4		elfz3	|- ( N e. ZZ -> N e. ( N ... N ) )
5		eleq1	|- ( k = N -> ( k e. ( N ... N ) <-> N e. ( N ... N ) ) )
6	4 5	syl5ibrcom	|- ( N e. ZZ -> ( k = N -> k e. ( N ... N ) ) )
7	3 6	impbid2	|- ( N e. ZZ -> ( k e. ( N ... N ) <-> k = N ) )
8	7	imbi1d	|- ( N e. ZZ -> ( ( k e. ( N ... N ) -> ph ) <-> ( k = N -> ph ) ) )
9	8	albidv	|- ( N e. ZZ -> ( A. k ( k e. ( N ... N ) -> ph ) <-> A. k ( k = N -> ph ) ) )
10	2 9	bitr2id	|- ( N e. ZZ -> ( A. k ( k = N -> ph ) <-> A. k e. ( N ... N ) ph ) )
11	1 10	bitr2d	|- ( N e. ZZ -> ( A. k e. ( N ... N ) ph <-> [. N / k ]. ph ) )