# 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 ${⊢}{M}\in ℤ\to \left(\forall {n}\in {ℤ}_{\ge {M}}\phantom{\rule{.4em}{0ex}}{\phi }↔\forall {n}\in ℤ\phantom{\rule{.4em}{0ex}}\left({M}\le {n}\to {\phi }\right)\right)$

### Proof

Step Hyp Ref Expression
1 eluz1 ${⊢}{M}\in ℤ\to \left({n}\in {ℤ}_{\ge {M}}↔\left({n}\in ℤ\wedge {M}\le {n}\right)\right)$
2 1 imbi1d ${⊢}{M}\in ℤ\to \left(\left({n}\in {ℤ}_{\ge {M}}\to {\phi }\right)↔\left(\left({n}\in ℤ\wedge {M}\le {n}\right)\to {\phi }\right)\right)$
3 impexp ${⊢}\left(\left({n}\in ℤ\wedge {M}\le {n}\right)\to {\phi }\right)↔\left({n}\in ℤ\to \left({M}\le {n}\to {\phi }\right)\right)$
4 2 3 syl6bb ${⊢}{M}\in ℤ\to \left(\left({n}\in {ℤ}_{\ge {M}}\to {\phi }\right)↔\left({n}\in ℤ\to \left({M}\le {n}\to {\phi }\right)\right)\right)$
5 4 ralbidv2 ${⊢}{M}\in ℤ\to \left(\forall {n}\in {ℤ}_{\ge {M}}\phantom{\rule{.4em}{0ex}}{\phi }↔\forall {n}\in ℤ\phantom{\rule{.4em}{0ex}}\left({M}\le {n}\to {\phi }\right)\right)$