Theorem rexuz2

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

	Ref	Expression
Assertion	rexuz2	⊢ ( ∃ 𝑛 ∈ ( ℤ≥ ‘ 𝑀 ) 𝜑 ↔ ( 𝑀 ∈ ℤ ∧ ∃ 𝑛 ∈ ℤ ( 𝑀 ≤ 𝑛 ∧ 𝜑 ) ) )

Proof

Step	Hyp	Ref	Expression
1		eluz2	⊢ ( 𝑛 ∈ ( ℤ≥ ‘ 𝑀 ) ↔ ( 𝑀 ∈ ℤ ∧ 𝑛 ∈ ℤ ∧ 𝑀 ≤ 𝑛 ) )
2		df-3an	⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑛 ∈ ℤ ∧ 𝑀 ≤ 𝑛 ) ↔ ( ( 𝑀 ∈ ℤ ∧ 𝑛 ∈ ℤ ) ∧ 𝑀 ≤ 𝑛 ) )
3	1 2	bitri	⊢ ( 𝑛 ∈ ( ℤ≥ ‘ 𝑀 ) ↔ ( ( 𝑀 ∈ ℤ ∧ 𝑛 ∈ ℤ ) ∧ 𝑀 ≤ 𝑛 ) )
4	3	anbi1i	⊢ ( ( 𝑛 ∈ ( ℤ≥ ‘ 𝑀 ) ∧ 𝜑 ) ↔ ( ( ( 𝑀 ∈ ℤ ∧ 𝑛 ∈ ℤ ) ∧ 𝑀 ≤ 𝑛 ) ∧ 𝜑 ) )
5		anass	⊢ ( ( ( ( 𝑀 ∈ ℤ ∧ 𝑛 ∈ ℤ ) ∧ 𝑀 ≤ 𝑛 ) ∧ 𝜑 ) ↔ ( ( 𝑀 ∈ ℤ ∧ 𝑛 ∈ ℤ ) ∧ ( 𝑀 ≤ 𝑛 ∧ 𝜑 ) ) )
6		an21	⊢ ( ( ( 𝑀 ∈ ℤ ∧ 𝑛 ∈ ℤ ) ∧ ( 𝑀 ≤ 𝑛 ∧ 𝜑 ) ) ↔ ( 𝑛 ∈ ℤ ∧ ( 𝑀 ∈ ℤ ∧ ( 𝑀 ≤ 𝑛 ∧ 𝜑 ) ) ) )
7	5 6	bitri	⊢ ( ( ( ( 𝑀 ∈ ℤ ∧ 𝑛 ∈ ℤ ) ∧ 𝑀 ≤ 𝑛 ) ∧ 𝜑 ) ↔ ( 𝑛 ∈ ℤ ∧ ( 𝑀 ∈ ℤ ∧ ( 𝑀 ≤ 𝑛 ∧ 𝜑 ) ) ) )
8	4 7	bitri	⊢ ( ( 𝑛 ∈ ( ℤ≥ ‘ 𝑀 ) ∧ 𝜑 ) ↔ ( 𝑛 ∈ ℤ ∧ ( 𝑀 ∈ ℤ ∧ ( 𝑀 ≤ 𝑛 ∧ 𝜑 ) ) ) )
9	8	rexbii2	⊢ ( ∃ 𝑛 ∈ ( ℤ≥ ‘ 𝑀 ) 𝜑 ↔ ∃ 𝑛 ∈ ℤ ( 𝑀 ∈ ℤ ∧ ( 𝑀 ≤ 𝑛 ∧ 𝜑 ) ) )
10		r19.42v	⊢ ( ∃ 𝑛 ∈ ℤ ( 𝑀 ∈ ℤ ∧ ( 𝑀 ≤ 𝑛 ∧ 𝜑 ) ) ↔ ( 𝑀 ∈ ℤ ∧ ∃ 𝑛 ∈ ℤ ( 𝑀 ≤ 𝑛 ∧ 𝜑 ) ) )
11	9 10	bitri	⊢ ( ∃ 𝑛 ∈ ( ℤ≥ ‘ 𝑀 ) 𝜑 ↔ ( 𝑀 ∈ ℤ ∧ ∃ 𝑛 ∈ ℤ ( 𝑀 ≤ 𝑛 ∧ 𝜑 ) ) )