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 ) ) )