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 \in ℤ \to (\forall k \in (N \dots N) φ \leftrightarrow \underset{˙}{[} N / k \underset{˙}{]} φ)$

Step	Hyp	Ref	Expression
1		sbc6g	$⊢ N \in ℤ \to (\underset{˙}{[} N / k \underset{˙}{]} φ \leftrightarrow \forall k (k = N \to φ))$
2		df-ral	$⊢ \forall k \in (N \dots N) φ \leftrightarrow \forall k (k \in (N \dots N) \to φ)$
3		elfz1eq	$⊢ k \in (N \dots N) \to k = N$
4		elfz3	$⊢ N \in ℤ \to N \in (N \dots N)$
5		eleq1	$⊢ k = N \to (k \in (N \dots N) \leftrightarrow N \in (N \dots N))$
6	4 5	syl5ibrcom	$⊢ N \in ℤ \to (k = N \to k \in (N \dots N))$
7	3 6	impbid2	$⊢ N \in ℤ \to (k \in (N \dots N) \leftrightarrow k = N)$
8	7	imbi1d	$⊢ N \in ℤ \to ((k \in (N \dots N) \to φ) \leftrightarrow (k = N \to φ))$
9	8	albidv	$⊢ N \in ℤ \to (\forall k (k \in (N \dots N) \to φ) \leftrightarrow \forall k (k = N \to φ))$
10	2 9	bitr2id	$⊢ N \in ℤ \to (\forall k (k = N \to φ) \leftrightarrow \forall k \in (N \dots N) φ)$
11	1 10	bitr2d	$⊢ N \in ℤ \to (\forall k \in (N \dots N) φ \leftrightarrow \underset{˙}{[} N / k \underset{˙}{]} φ)$

Metamath Proof Explorer