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 ( 𝑁 ∈ ℤ → ( ∀ 𝑘 ∈ ( 𝑁 ... 𝑁 ) 𝜑 ↔ [ 𝑁 / 𝑘 ] 𝜑 ) )

Proof

Step Hyp Ref Expression
1 sbc6g ⊢ ( 𝑁 ∈ ℤ → ( [ 𝑁 / 𝑘 ] 𝜑 ↔ ∀ 𝑘 ( 𝑘 = 𝑁 → 𝜑 ) ) )
2 df-ral ⊢ ( ∀ 𝑘 ∈ ( 𝑁 ... 𝑁 ) 𝜑 ↔ ∀ 𝑘 ( 𝑘 ∈ ( 𝑁 ... 𝑁 ) → 𝜑 ) )
3 elfz1eq ⊢ ( 𝑘 ∈ ( 𝑁 ... 𝑁 ) → 𝑘 = 𝑁 )
4 elfz3 ⊢ ( 𝑁 ∈ ℤ → 𝑁 ∈ ( 𝑁 ... 𝑁 ) )
5 eleq1 ⊢ ( 𝑘 = 𝑁 → ( 𝑘 ∈ ( 𝑁 ... 𝑁 ) ↔ 𝑁 ∈ ( 𝑁 ... 𝑁 ) ) )
6 4 5 syl5ibrcom ⊢ ( 𝑁 ∈ ℤ → ( 𝑘 = 𝑁 → 𝑘 ∈ ( 𝑁 ... 𝑁 ) ) )
7 3 6 impbid2 ⊢ ( 𝑁 ∈ ℤ → ( 𝑘 ∈ ( 𝑁 ... 𝑁 ) ↔ 𝑘 = 𝑁 ) )
8 7 imbi1d ⊢ ( 𝑁 ∈ ℤ → ( ( 𝑘 ∈ ( 𝑁 ... 𝑁 ) → 𝜑 ) ↔ ( 𝑘 = 𝑁 → 𝜑 ) ) )
9 8 albidv ⊢ ( 𝑁 ∈ ℤ → ( ∀ 𝑘 ( 𝑘 ∈ ( 𝑁 ... 𝑁 ) → 𝜑 ) ↔ ∀ 𝑘 ( 𝑘 = 𝑁 → 𝜑 ) ) )
10 2 9 bitr2id ⊢ ( 𝑁 ∈ ℤ → ( ∀ 𝑘 ( 𝑘 = 𝑁 → 𝜑 ) ↔ ∀ 𝑘 ∈ ( 𝑁 ... 𝑁 ) 𝜑 ) )
11 1 10 bitr2d ⊢ ( 𝑁 ∈ ℤ → ( ∀ 𝑘 ∈ ( 𝑁 ... 𝑁 ) 𝜑 ↔ [ 𝑁 / 𝑘 ] 𝜑 ) )