Theorem 2rexuz

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

	Ref	Expression
Assertion	2rexuz	⊢ ( ∃ 𝑚 ∃ 𝑛 ∈ ( ℤ≥ ‘ 𝑚 ) 𝜑 ↔ ∃ 𝑚 ∈ ℤ ∃ 𝑛 ∈ ℤ ( 𝑚 ≤ 𝑛 ∧ 𝜑 ) )

Proof

Step	Hyp	Ref	Expression
1		rexuz2	⊢ ( ∃ 𝑛 ∈ ( ℤ≥ ‘ 𝑚 ) 𝜑 ↔ ( 𝑚 ∈ ℤ ∧ ∃ 𝑛 ∈ ℤ ( 𝑚 ≤ 𝑛 ∧ 𝜑 ) ) )
2	1	exbii	⊢ ( ∃ 𝑚 ∃ 𝑛 ∈ ( ℤ≥ ‘ 𝑚 ) 𝜑 ↔ ∃ 𝑚 ( 𝑚 ∈ ℤ ∧ ∃ 𝑛 ∈ ℤ ( 𝑚 ≤ 𝑛 ∧ 𝜑 ) ) )
3		df-rex	⊢ ( ∃ 𝑚 ∈ ℤ ∃ 𝑛 ∈ ℤ ( 𝑚 ≤ 𝑛 ∧ 𝜑 ) ↔ ∃ 𝑚 ( 𝑚 ∈ ℤ ∧ ∃ 𝑛 ∈ ℤ ( 𝑚 ≤ 𝑛 ∧ 𝜑 ) ) )
4	2 3	bitr4i	⊢ ( ∃ 𝑚 ∃ 𝑛 ∈ ( ℤ≥ ‘ 𝑚 ) 𝜑 ↔ ∃ 𝑚 ∈ ℤ ∃ 𝑛 ∈ ℤ ( 𝑚 ≤ 𝑛 ∧ 𝜑 ) )