rexuz2

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

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

Step	Hyp	Ref	Expression
1		eluz2	$⊢ n \in ℤ_{\geq M} \leftrightarrow (M \in ℤ \land n \in ℤ \land M \leq n)$
2		df-3an	$⊢ (M \in ℤ \land n \in ℤ \land M \leq n) \leftrightarrow ((M \in ℤ \land n \in ℤ) \land M \leq n)$
3	1 2	bitri	$⊢ n \in ℤ_{\geq M} \leftrightarrow ((M \in ℤ \land n \in ℤ) \land M \leq n)$
4	3	anbi1i	$⊢ (n \in ℤ_{\geq M} \land φ) \leftrightarrow (((M \in ℤ \land n \in ℤ) \land M \leq n) \land φ)$
5		anass	$⊢ (((M \in ℤ \land n \in ℤ) \land M \leq n) \land φ) \leftrightarrow ((M \in ℤ \land n \in ℤ) \land (M \leq n \land φ))$
6		an21	$⊢ ((M \in ℤ \land n \in ℤ) \land (M \leq n \land φ)) \leftrightarrow (n \in ℤ \land (M \in ℤ \land (M \leq n \land φ)))$
7	5 6	bitri	$⊢ (((M \in ℤ \land n \in ℤ) \land M \leq n) \land φ) \leftrightarrow (n \in ℤ \land (M \in ℤ \land (M \leq n \land φ)))$
8	4 7	bitri	$⊢ (n \in ℤ_{\geq M} \land φ) \leftrightarrow (n \in ℤ \land (M \in ℤ \land (M \leq n \land φ)))$
9	8	rexbii2	$⊢ \exists n \in ℤ_{\geq M} φ \leftrightarrow \exists n \in ℤ (M \in ℤ \land (M \leq n \land φ))$
10		r19.42v	$⊢ \exists n \in ℤ (M \in ℤ \land (M \leq n \land φ)) \leftrightarrow (M \in ℤ \land \exists n \in ℤ (M \leq n \land φ))$
11	9 10	bitri	$⊢ \exists n \in ℤ_{\geq M} φ \leftrightarrow (M \in ℤ \land \exists n \in ℤ (M \leq n \land φ))$

Metamath Proof Explorer