Theorem rexuz

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

	Ref	Expression
Assertion	rexuz	|- ( M e. ZZ -> ( E. n e. ( ZZ>= ` M ) ph <-> E. 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	anbi1d	|- ( M e. ZZ -> ( ( n e. ( ZZ>= ` M ) /\ ph ) <-> ( ( n e. ZZ /\ M <_ n ) /\ ph ) ) )
3		anass	|- ( ( ( 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	rexbidv2	|- ( M e. ZZ -> ( E. n e. ( ZZ>= ` M ) ph <-> E. n e. ZZ ( M <_ n /\ ph ) ) )