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 ∈ ℤ → ∀ k ∈ N … N φ ↔ [˙N / k]˙ φ

Proof

Step Hyp Ref Expression
1 sbc6g ⊢ N ∈ ℤ → [˙N / k]˙ φ ↔ ∀ k k = N → φ
2 df-ral ⊢ ∀ k ∈ N … N φ ↔ ∀ k k ∈ N … N → φ
3 elfz1eq ⊢ k ∈ N … N → k = N
4 elfz3 ⊢ N ∈ ℤ → N ∈ N … N
5 eleq1 ⊢ k = N → k ∈ N … N ↔ N ∈ N … N
6 4 5 syl5ibrcom ⊢ N ∈ ℤ → k = N → k ∈ N … N
7 3 6 impbid2 ⊢ N ∈ ℤ → k ∈ N … N ↔ k = N
8 7 imbi1d ⊢ N ∈ ℤ → k ∈ N … N → φ ↔ k = N → φ
9 8 albidv ⊢ N ∈ ℤ → ∀ k k ∈ N … N → φ ↔ ∀ k k = N → φ
10 2 9 bitr2id ⊢ N ∈ ℤ → ∀ k k = N → φ ↔ ∀ k ∈ N … N φ
11 1 10 bitr2d ⊢ N ∈ ℤ → ∀ k ∈ N … N φ ↔ [˙N / k]˙ φ