Theorem 2rexuz

Description: Double existential quantification in an upper set of integers. (Contributed by NM, 3-Nov-2005)

	Ref	Expression
Assertion	2rexuz	|- ( E. m E. n e. ( ZZ>= ` m ) ph <-> E. m e. ZZ E. n e. ZZ ( m <_ n /\ ph ) )

Proof

Step	Hyp	Ref	Expression
1		rexuz2	|- ( E. n e. ( ZZ>= ` m ) ph <-> ( m e. ZZ /\ E. n e. ZZ ( m <_ n /\ ph ) ) )
2	1	exbii	|- ( E. m E. n e. ( ZZ>= ` m ) ph <-> E. m ( m e. ZZ /\ E. n e. ZZ ( m <_ n /\ ph ) ) )
3		df-rex	|- ( E. m e. ZZ E. n e. ZZ ( m <_ n /\ ph ) <-> E. m ( m e. ZZ /\ E. n e. ZZ ( m <_ n /\ ph ) ) )
4	2 3	bitr4i	|- ( E. m E. n e. ( ZZ>= ` m ) ph <-> E. m e. ZZ E. n e. ZZ ( m <_ n /\ ph ) )