Metamath Proof Explorer


Theorem raluz

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

Ref Expression
Assertion raluz ( 𝑀 ∈ ℤ → ( ∀ 𝑛 ∈ ( ℤ𝑀 ) 𝜑 ↔ ∀ 𝑛 ∈ ℤ ( 𝑀𝑛𝜑 ) ) )

Proof

Step Hyp Ref Expression
1 eluz1 ( 𝑀 ∈ ℤ → ( 𝑛 ∈ ( ℤ𝑀 ) ↔ ( 𝑛 ∈ ℤ ∧ 𝑀𝑛 ) ) )
2 1 imbi1d ( 𝑀 ∈ ℤ → ( ( 𝑛 ∈ ( ℤ𝑀 ) → 𝜑 ) ↔ ( ( 𝑛 ∈ ℤ ∧ 𝑀𝑛 ) → 𝜑 ) ) )
3 impexp ( ( ( 𝑛 ∈ ℤ ∧ 𝑀𝑛 ) → 𝜑 ) ↔ ( 𝑛 ∈ ℤ → ( 𝑀𝑛𝜑 ) ) )
4 2 3 bitrdi ( 𝑀 ∈ ℤ → ( ( 𝑛 ∈ ( ℤ𝑀 ) → 𝜑 ) ↔ ( 𝑛 ∈ ℤ → ( 𝑀𝑛𝜑 ) ) ) )
5 4 ralbidv2 ( 𝑀 ∈ ℤ → ( ∀ 𝑛 ∈ ( ℤ𝑀 ) 𝜑 ↔ ∀ 𝑛 ∈ ℤ ( 𝑀𝑛𝜑 ) ) )