Theorem rexlimdvva 2878

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 441	. 2 |- ( ph -> ( ( x e. A /\ y e. B ) -> ( ps -> ch ) ) )
3	2	rexlimdvv 2877	1 |- ( ph -> ( E. x e. A E. y e. B ps -> ch ) )

Syntax hints:   -> wi 4   /\ wa 376   e. wcel 1904   E.wrex 2757

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1677  ax-4 1690  ax-5 1766

This theorem depends on definitions:  df-bi 190  df-an 378  df-ex 1672  df-ral 2761  df-rex 2762

This theorem is referenced by:  disjxiun  4392  f1prex  6200  f1o2ndf1  6923  uniinqs  7461  eroveu  7476  eroprf  7479  ralxpmap  7539  unxpdomlem3  7796  finsschain  7899  dffi3  7963  sornom  8725  genpv  9442  genpdm  9445  1re  9660  cnegex  9832  zaddcl  11001  rexanre  13486  o1lo1  13678  lo1resb  13705  o1resb  13707  rlimcn2  13731  climcn2  13733  o1of2  13753  o1rlimmul  13759  lo1add  13767  lo1mul  13768  summo  13860  o1fsum  13950  ntrivcvgmul  14035  prodmolem2  14066  prodmo  14067  dvds2lem  14392  bezoutlem4OLD  14585  bezoutlem4  14588  dvdsmulgcd  14601  pcqmul  14882  pcneg  14902  pcadd  14913  4sqlem1  14971  4sqlem2  14972  4sqlem4  14975  mul4sq  14977  4sqlem12  14979  4sqlem13OLD  14980  4sqlem18OLD  14985  4sqlem13  14986  4sqlem18  14991  vdwmc2  15008  vdwlem7  15016  vdwlem9  15018  vdwlem10  15019  vdwlem11  15020  ramlb  15056  ramub1lem2  15064  imasaddfnlem  15512  imasmnd2  16651  imasgrp2  16879  gaorber  17040  psgnunilem2  17214  psgneu  17225  lsmsubm  17383  lsmsubg  17384  lsmmod  17403  lsmdisj2  17410  pj1eu  17424  efgtlen  17454  efgredlem  17475  efgredeu  17480  efgcpbllemb  17483  frgpuptinv  17499  frgpup3lem  17505  qusabl  17581  frgpnabllem1  17587  frgpnabl  17589  cygabl  17603  dprdsubg  17735  ablfacrp  17777  pgpfac1lem3  17788  imasring  17925  dvdsrtr  17958  lss1d  18264  lsmcl  18384  lsmelval2  18386  lbsextlem2  18460  isnzr2  18564  qsssubdrg  19104  znfld  19208  cygznlem3  19217  psgnghm  19225  lsmcss  19332  mdetunilem7  19720  mdetunilem8  19721  cayleyhamilton0  19990  cayleyhamiltonALT  19992  restbas  20251  ordtbas2  20284  ordtbas  20285  cnhaus  20447  cldllycmp  20587  txbas  20659  ptbasin  20669  txcls  20696  xkoccn  20711  txindis  20726  txlly  20728  txnlly  20729  pthaus  20730  ptrescn  20731  txhaus  20739  tx1stc  20742  txkgen  20744  xkohaus  20745  xkoptsub  20746  xkopt  20747  xkoco1cn  20749  xkoco2cn  20750  xkoinjcn  20779  fmfnfmlem3  21049  fmfnfmlem4  21050  hausflimi  21073  hauspwpwf1  21080  txflf  21099  qustgplem  21213  blin2  21522  prdsxmslem2  21622  xrge0tsms  21930  addcnlem  21974  minveclem3b  22448  minveclem3bOLD  22460  pmltpc  22479  evthicc2  22489  dyaddisj  22633  ismbfd  22675  mbfimaopnlem  22690  rolle  23021  dvcnvrelem1  23048  dvcvx  23051  itgsubst  23080  plyf  23231  plypf1  23245  plyadd  23250  plymul  23251  coeeu  23258  dgrlem  23262  coeid  23271  aalioulem6  23372  o1cxp  23979  dchrptlem2  24272  lgsdchr  24355  2sqlem5  24375  2sqlem9  24380  2sqb  24385  pntlemp  24527  pnt3  24529  ostthlem1  24544  ostth3  24555  axcontlem4  25076  axcontlem9  25081  sizeusglecusglem1  25291  el2wlksotot  25689  3cyclfrgra  25822  n4cyclfrgra  25825  frgrawopreg  25856  ubthlem3  26595  cdjreui  28166  cdj3i  28175  br8d  28294  xrofsup  28428  xrge0tsmsd  28622  qqhval2  28860  mbfmco2  29160  txpcon  30027  cvmlift2lem10  30107  cvmlift2lem12  30109  cvmlift3lem7  30120  cvmlift3lem8  30121  mclsppslem  30293  br8  30467  br6  30468  br4  30469  brsegle  30946  tailfb  31104  mblfinlem3  32043  ismblfin  32045  itg2addnc  32060  ftc1anc  32089  isbnd2  32179  isbnd3  32180  ssbnd  32184  ispridlc  32367  lshpkrlem6  32752  athgt  33092  3dim1  33103  3dim2  33104  lvolex3N  33174  llncvrlpln2  33193  lplncvrlvol2  33251  linepsubN  33388  lncvrelatN  33417  linepsubclN  33587  eldioph2  35675  eldioph2b  35676  diophin  35686  diophun  35687  fphpdo  35731  irrapxlem3  35739  irrapxlem5  35741  pell1234qrne0  35770  pell1234qrreccl  35771  pell1234qrmulcl  35772  pell14qrgt0  35776  pell14qrdich  35786  pell1qrge1  35787  pell1qrgap  35791  pellqrex  35797  rmxycomplete  35836  jm2.27  35934  stoweidlem49  38022  gbogt5  39008  usgredg4  39458  nbuhgr2vtx1edgb  39584  2pthon3v-av  40065  umgr3v3e3cycl  40098  m1modmmod  40832