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 e. ZZ -> ( A. n e. ( ZZ>= ` M ) ph <-> A. n e. ZZ ( M <_ n -> ph ) ) )

Proof

Step Hyp Ref Expression
1 eluz1
 |-  ( M e. ZZ -> ( n e. ( ZZ>= ` M ) <-> ( n e. ZZ /\ M <_ n ) ) )
2 1 imbi1d
 |-  ( M e. ZZ -> ( ( n e. ( ZZ>= ` M ) -> ph ) <-> ( ( n e. ZZ /\ M <_ n ) -> ph ) ) )
3 impexp
 |-  ( ( ( n e. ZZ /\ M <_ n ) -> ph ) <-> ( n e. ZZ -> ( M <_ n -> ph ) ) )
4 2 3 bitrdi
 |-  ( M e. ZZ -> ( ( n e. ( ZZ>= ` M ) -> ph ) <-> ( n e. ZZ -> ( M <_ n -> ph ) ) ) )
5 4 ralbidv2
 |-  ( M e. ZZ -> ( A. n e. ( ZZ>= ` M ) ph <-> A. n e. ZZ ( M <_ n -> ph ) ) )