Theorem rexlimdvva 2886

Description: Inference from Theorem 19.23 of [Margaris] p. 90. (Restricted quantifier version.) (Contributed by NM, 18-Jun-2014.)

Hypothesis

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

Assertion

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

Distinct variable groups:   x, y, ph   ch, x, y   y, A

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

Proof of Theorem rexlimdvva

Step	Hyp	Ref	Expression
1		rexlimdvva.1	. . 3 |- ( ( ph /\ ( x e. A /\ y e. B ) ) -> ( ps -> ch ) )
2	1	ex 436	. 2 |- ( ph -> ( ( x e. A /\ y e. B ) -> ( ps -> ch ) ) )
3	2	rexlimdvv 2885	1 |- ( ph -> ( E. x e. A E. y e. B ps -> ch ) )

Syntax hints:   -> wi 4   /\ wa 371   e. wcel 1887   E.wrex 2738

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1669  ax-4 1682  ax-5 1758

This theorem depends on definitions:  df-bi 189  df-an 373  df-ex 1664  df-ral 2742  df-rex 2743

This theorem is referenced by:  disjxiun  4399  f1prex  6182  f1o2ndf1  6904  uniinqs  7443  eroveu  7458  eroprf  7461  ralxpmap  7521  unxpdomlem3  7778  finsschain  7881  dffi3  7945  sornom  8707  genpv  9424  genpdm  9427  1re  9642  cnegex  9814  zaddcl  10977  rexanre  13409  o1lo1  13601  lo1resb  13628  o1resb  13630  rlimcn2  13654  climcn2  13656  o1of2  13676  o1rlimmul  13682  lo1add  13690  lo1mul  13691  summo  13783  o1fsum  13873  ntrivcvgmul  13958  prodmolem2  13989  prodmo  13990  dvds2lem  14315  bezoutlem4OLD  14506  bezoutlem4  14509  dvdsmulgcd  14522  pcqmul  14803  pcneg  14823  pcadd  14834  4sqlem1  14892  4sqlem2  14893  4sqlem4  14896  mul4sq  14898  4sqlem12  14900  4sqlem13OLD  14901  4sqlem18OLD  14906  4sqlem13  14907  4sqlem18  14912  vdwmc2  14929  vdwlem7  14937  vdwlem9  14939  vdwlem10  14940  vdwlem11  14941  ramlb  14977  ramub1lem2  14985  imasaddfnlem  15434  imasmnd2  16573  imasgrp2  16801  gaorber  16962  psgnunilem2  17136  psgneu  17147  lsmsubm  17305  lsmsubg  17306  lsmmod  17325  lsmdisj2  17332  pj1eu  17346  efgtlen  17376  efgredlem  17397  efgredeu  17402  efgcpbllemb  17405  frgpuptinv  17421  frgpup3lem  17427  qusabl  17503  frgpnabllem1  17509  frgpnabl  17511  cygabl  17525  dprdsubg  17657  ablfacrp  17699  pgpfac1lem3  17710  imasring  17847  dvdsrtr  17880  lss1d  18186  lsmcl  18306  lsmelval2  18308  lbsextlem2  18382  isnzr2  18487  qsssubdrg  19027  znfld  19131  cygznlem3  19140  psgnghm  19148  lsmcss  19255  mdetunilem7  19643  mdetunilem8  19644  cayleyhamilton0  19913  cayleyhamiltonALT  19915  restbas  20174  ordtbas2  20207  ordtbas  20208  cnhaus  20370  cldllycmp  20510  txbas  20582  ptbasin  20592  txcls  20619  xkoccn  20634  txindis  20649  txlly  20651  txnlly  20652  pthaus  20653  ptrescn  20654  txhaus  20662  tx1stc  20665  txkgen  20667  xkohaus  20668  xkoptsub  20669  xkopt  20670  xkoco1cn  20672  xkoco2cn  20673  xkoinjcn  20702  fmfnfmlem3  20971  fmfnfmlem4  20972  hausflimi  20995  hauspwpwf1  21002  txflf  21021  qustgplem  21135  blin2  21444  prdsxmslem2  21544  xrge0tsms  21852  addcnlem  21896  minveclem3b  22370  minveclem3bOLD  22382  pmltpc  22401  evthicc2  22411  dyaddisj  22554  ismbfd  22596  mbfimaopnlem  22611  rolle  22942  dvcnvrelem1  22969  dvcvx  22972  itgsubst  23001  plyf  23152  plypf1  23166  plyadd  23171  plymul  23172  coeeu  23179  dgrlem  23183  coeid  23192  aalioulem6  23293  o1cxp  23900  dchrptlem2  24193  lgsdchr  24276  2sqlem5  24296  2sqlem9  24301  2sqb  24306  pntlemp  24448  pnt3  24450  ostthlem1  24465  ostth3  24476  axcontlem4  24997  axcontlem9  25002  sizeusglecusglem1  25212  el2wlksotot  25610  3cyclfrgra  25743  n4cyclfrgra  25746  frgrawopreg  25777  ubthlem3  26514  cdjreui  28085  cdj3i  28094  br8d  28218  xrofsup  28353  xrge0tsmsd  28548  qqhval2  28786  mbfmco2  29087  txpcon  29955  cvmlift2lem10  30035  cvmlift2lem12  30037  cvmlift3lem7  30048  cvmlift3lem8  30049  mclsppslem  30221  br8  30396  br6  30397  br4  30398  brsegle  30875  tailfb  31033  mblfinlem3  31979  ismblfin  31981  itg2addnc  31996  ftc1anc  32025  isbnd2  32115  isbnd3  32116  ssbnd  32120  ispridlc  32303  lshpkrlem6  32681  athgt  33021  3dim1  33032  3dim2  33033  lvolex3N  33103  llncvrlpln2  33122  lplncvrlvol2  33180  linepsubN  33317  lncvrelatN  33346  linepsubclN  33516  eldioph2  35604  eldioph2b  35605  diophin  35615  diophun  35616  fphpdo  35660  irrapxlem3  35668  irrapxlem5  35670  pell1234qrne0  35699  pell1234qrreccl  35700  pell1234qrmulcl  35701  pell14qrgt0  35705  pell14qrdich  35715  pell1qrge1  35716  pell1qrgap  35720  pellqrex  35726  rmxycomplete  35765  jm2.27  35863  stoweidlem49  37910  gbogt5  38863  usgredg4  39294  nbgr2vtx1edg  39418  nbuhgr2vtx1edgb  39420  m1modmmod  40377