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φ↔∃mm∈ℤ∧∃n∈ℤm≤n∧φ
3 df-rex ⊢∃m∈ℤ∃n∈ℤm≤n∧φ↔∃mm∈ℤ∧∃n∈ℤm≤n∧φ
4 2 3 bitr4i ⊢∃m∃n∈ℤ≥mφ↔∃m∈ℤ∃n∈ℤm≤n∧φ