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