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

Metamath Proof Explorer

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 ) )