Theorem rexlimivv 3036

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 3031	. 2 |- ( x e. A -> ( E. y e. B ph -> ps ) )
3	2	rexlimiv 3027	1 |- ( E. x e. A E. y e. B ph -> ps )

Syntax hints:   -> wi 4   /\ wa 384   e. wcel 1990   E.wrex 2913

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839

This theorem depends on definitions:  df-bi 197  df-an 386  df-ex 1705  df-ral 2917  df-rex 2918

This theorem is referenced by:  2reu5  3416  opelxp  5146  opiota  7229  f1o2ndf1  7285  tfrlem5  7476  xpdom2  8055  1sdom  8163  unxpdomlem3  8166  unfi  8227  elfiun  8336  xpnum  8777  kmlem9  8980  nqereu  9751  distrlem5pr  9849  mulid1  10037  1re  10039  mul02  10214  cnegex  10217  recex  10659  creur  11014  creui  11015  cju  11016  elz2  11394  zaddcl  11417  qre  11793  qaddcl  11804  qnegcl  11805  qmulcl  11806  qreccl  11808  hash2prd  13257  elss2prb  13269  fundmge2nop0  13274  wrdl3s3  13705  replim  13856  prodmo  14666  odd2np1  15065  opoe  15087  omoe  15088  opeo  15089  omeo  15090  qredeu  15372  pythagtriplem1  15521  pcz  15585  4sqlem1  15652  4sqlem2  15653  4sqlem4  15656  mul4sq  15658  pmtr3ncom  17895  efgmnvl  18127  efgrelexlema  18162  ring1ne0  18591  txuni2  21368  tx2ndc  21454  blssioo  22598  tgioo  22599  ioorf  23341  ioorinv  23344  ioorcl  23345  dyaddisj  23364  mbfid  23403  elply  23951  vmacl  24844  efvmacl  24846  vmalelog  24930  2sqlem2  25143  mul2sq  25144  2sqlem7  25149  pntibnd  25282  ostth  25328  legval  25479  upgredgpr  26037  nbgr2vtx1edg  26246  uvtx2vtx1edg  26299  cusgredg  26320  usgredgsscusgredg  26355  n4cyclfrgr  27155  vdgn1frgrv2  27160  friendshipgt3  27256  lpni  27332  nsnlplig  27333  nsnlpligALT  27334  n0lpligALT  27336  ipasslem5  27690  ipasslem11  27695  hhssnv  28121  shscli  28176  shsleji  28229  shsidmi  28243  spansncvi  28511  superpos  29213  chirredi  29253  mdsymlem6  29267  rnmpt2ss  29473  cnre2csqima  29957  dya2icobrsiga  30338  dya2iocnrect  30343  dya2iocucvr  30346  sxbrsigalem2  30348  afsval  30749  msubco  31428  poseq  31750  soseq  31751  scutf  31919  elaltxp  32082  altxpsspw  32084  funtransport  32138  funray  32247  funline  32249  ellines  32259  linethru  32260  icoreresf  33200  icoreclin  33205  relowlssretop  33211  relowlpssretop  33212  itg2addnc  33464  isline  35025  mzpcompact2lem  37314  2reu4  41190  nnsum3primesgbe  41680  nnsum4primesodd  41684  nnsum4primesoddALTV  41685  tgblthelfgott  41703  sprvalpw  41730  sprvalpwn0  41733  prsprel  41737  nnpw2pb  42381