This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ∧ φ