Metamath Proof Explorer

Theorem 2rexuz

Description: Double existential quantification in an upper set of integers. (Contributed by NM, 3-Nov-2005)

Ref Expression
Assertion 2rexuz ⊢ ∃ m ∃ n ∈ ℤ ≥ m φ ↔ ∃ m ∈ ℤ ∃ n ∈ ℤ m ≤ n ∧ φ

Proof

Step Hyp Ref Expression
1 rexuz2 ⊢ ∃ n ∈ ℤ ≥ m φ ↔ m ∈ ℤ ∧ ∃ n ∈ ℤ m ≤ n ∧ φ
2 1 exbii ⊢ ∃ m ∃ n ∈ ℤ ≥ m φ ↔ ∃ m m ∈ ℤ ∧ ∃ n ∈ ℤ m ≤ n ∧ φ
3 df-rex ⊢ ∃ m ∈ ℤ ∃ n ∈ ℤ m ≤ n ∧ φ ↔ ∃ m m ∈ ℤ ∧ ∃ n ∈ ℤ m ≤ n ∧ φ
4 2 3 bitr4i ⊢ ∃ m ∃ n ∈ ℤ ≥ m φ ↔ ∃ m ∈ ℤ ∃ n ∈ ℤ m ≤ n ∧ φ