raluz

Description: Restricted universal quantification in an upper set of integers. (Contributed by NM, 9-Sep-2005)

		Ref	Expression
	Assertion	raluz	$⊢ M \in ℤ \to (\forall n \in ℤ_{\geq M} φ \leftrightarrow \forall n \in ℤ (M \leq n \to φ))$

Step	Hyp	Ref	Expression
1		eluz1	$⊢ M \in ℤ \to (n \in ℤ_{\geq M} \leftrightarrow (n \in ℤ \land M \leq n))$
2	1	imbi1d	$⊢ M \in ℤ \to ((n \in ℤ_{\geq M} \to φ) \leftrightarrow ((n \in ℤ \land M \leq n) \to φ))$
3		impexp	$⊢ ((n \in ℤ \land M \leq n) \to φ) \leftrightarrow (n \in ℤ \to (M \leq n \to φ))$
4	2 3	bitrdi	$⊢ M \in ℤ \to ((n \in ℤ_{\geq M} \to φ) \leftrightarrow (n \in ℤ \to (M \leq n \to φ)))$
5	4	ralbidv2	$⊢ M \in ℤ \to (\forall n \in ℤ_{\geq M} φ \leftrightarrow \forall n \in ℤ (M \leq n \to φ))$

Metamath Proof Explorer