Theorem rexlimivv 2629

Description: Inference from Theorem 19.23 of [Margaris] p. 90 (restricted quantifier version). (Contributed by NM, 17-Feb-2004.)

Hypothesis

Ref	Expression
rexlimivv.1	|- ( ( x e. A /\ y e. B ) -> ( ph -> ps ) )

Assertion

Ref	Expression
rexlimivv	|- ( E. x e. A E. y e. B ph -> ps )

Distinct variable groups:   x, y, ps   y, A

Allowed substitution hints:   ph( x, y)   A( x)   B( x, y)

Proof of Theorem rexlimivv

Step	Hyp	Ref	Expression
1		rexlimivv.1	. . 3 |- ( ( x e. A /\ y e. B ) -> ( ph -> ps ) )
2	1	rexlimdva 2623	. 2 |- ( x e. A -> ( E. y e. B ph -> ps ) )
3	2	rexlimiv 2617	1 |- ( E. x e. A E. y e. B ph -> ps )

Syntax hints:   -> wi 4   /\ wa 104   e. wcel 2176   E.wrex 2485

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1470  ax-gen 1472  ax-ie1 1516  ax-ie2 1517  ax-4 1533  ax-17 1549  ax-ial 1557  ax-i5r 1558

This theorem depends on definitions:  df-bi 117  df-nf 1484  df-ral 2489  df-rex 2490

This theorem is referenced by:  opelxp  4705  f1o2ndf1  6314  xpdom2  6926  distrlem5prl  7699  distrlem5pru  7700  mulrid  8069  cnegex  8250  recexap  8726  creur  9032  creui  9033  cju  9034  elz2  9444  qre  9746  qaddcl  9756  qnegcl  9757  qmulcl  9758  qreccl  9763  elpqb  9771  fundm2domnop0  10990  replim  11170  prodmodc  11889  odd2np1  12184  opoe  12206  omoe  12207  opeo  12208  omeo  12209  qredeu  12419  pythagtriplem1  12588  pcz  12655  4sqlem1  12711  4sqlem2  12712  4sqlem4  12715  mul4sq  12717  txuni2  14728  blssioo  15025  tgioo  15026  elply  15206  2sqlem2  15592  mul2sq  15593  2sqlem7  15598