rexuz

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

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

Step	Hyp	Ref	Expression
1		eluz1	$⊢ M \in ℤ \to (n \in ℤ_{\geq M} \leftrightarrow (n \in ℤ \land M \leq n))$
2	1	anbi1d	$⊢ M \in ℤ \to ((n \in ℤ_{\geq M} \land φ) \leftrightarrow ((n \in ℤ \land M \leq n) \land φ))$
3		anass	$⊢ ((n \in ℤ \land M \leq n) \land φ) \leftrightarrow (n \in ℤ \land (M \leq n \land φ))$
4	2 3	bitrdi	$⊢ M \in ℤ \to ((n \in ℤ_{\geq M} \land φ) \leftrightarrow (n \in ℤ \land (M \leq n \land φ)))$
5	4	rexbidv2	$⊢ M \in ℤ \to (\exists n \in ℤ_{\geq M} φ \leftrightarrow \exists n \in ℤ (M \leq n \land φ))$

Metamath Proof Explorer