Theorem rexlimdvva 3038

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

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:  disjxiun  4649  disjxiunOLD  4650  f1prex  6539  f1o2ndf1  7285  uniinqs  7827  eroveu  7842  eroprf  7845  ralxpmap  7907  unxpdomlem3  8166  finsschain  8273  dffi3  8337  sornom  9099  genpv  9821  genpdm  9824  1re  10039  cnegex  10217  zaddcl  11417  rexanre  14086  o1lo1  14268  lo1resb  14295  o1resb  14297  rlimcn2  14321  climcn2  14323  o1of2  14343  o1rlimmul  14349  lo1add  14357  lo1mul  14358  summo  14448  o1fsum  14545  ntrivcvgmul  14634  prodmolem2  14665  prodmo  14666  dvds2lem  14994  bezoutlem4  15259  dvdsmulgcd  15274  divgcdcoprm0  15379  cncongr1  15381  pcqmul  15558  pcneg  15578  pcadd  15593  4sqlem1  15652  4sqlem2  15653  4sqlem4  15656  mul4sq  15658  4sqlem12  15660  4sqlem13  15661  4sqlem18  15666  vdwmc2  15683  vdwlem7  15691  vdwlem9  15693  vdwlem10  15694  vdwlem11  15695  ramlb  15723  ramub1lem2  15731  imasaddfnlem  16188  imasmnd2  17327  imasgrp2  17530  gaorber  17741  psgnunilem2  17915  psgneu  17926  lsmsubm  18068  lsmsubg  18069  lsmmod  18088  lsmdisj2  18095  pj1eu  18109  efgtlen  18139  efgredlem  18160  efgredeu  18165  efgcpbllemb  18168  frgpuptinv  18184  frgpup3lem  18190  qusabl  18268  frgpnabllem1  18276  frgpnabl  18278  cygabl  18292  dprdsubg  18423  ablfacrp  18465  pgpfac1lem3  18476  imasring  18619  dvdsrtr  18652  lss1d  18963  lsmcl  19083  lsmelval2  19085  lbsextlem2  19159  isnzr2  19263  qsssubdrg  19805  znfld  19909  cygznlem3  19918  psgnghm  19926  lsmcss  20036  mdetunilem7  20424  mdetunilem8  20425  cayleyhamilton0  20694  cayleyhamiltonALT  20696  restbas  20962  ordtbas2  20995  ordtbas  20996  cnhaus  21158  cldllycmp  21298  txbas  21370  ptbasin  21380  txcls  21407  xkoccn  21422  txindis  21437  txlly  21439  txnlly  21440  pthaus  21441  ptrescn  21442  txhaus  21450  tx1stc  21453  txkgen  21455  xkohaus  21456  xkoptsub  21457  xkopt  21458  xkoco1cn  21460  xkoco2cn  21461  xkoinjcn  21490  fmfnfmlem3  21760  fmfnfmlem4  21761  hausflimi  21784  hauspwpwf1  21791  txflf  21810  qustgplem  21924  blin2  22234  prdsxmslem2  22334  xrge0tsms  22637  addcnlem  22667  minveclem3b  23199  pmltpc  23219  evthicc2  23229  dyaddisj  23364  ismbfd  23407  mbfimaopnlem  23422  rolle  23753  dvcnvrelem1  23780  dvcvx  23783  itgsubst  23812  plyf  23954  plypf1  23968  plyadd  23973  plymul  23974  coeeu  23981  dgrlem  23985  coeid  23994  aalioulem6  24092  o1cxp  24701  dchrptlem2  24990  lgsdchr  25080  2sqlem5  25147  2sqlem9  25152  2sqb  25157  pntlemp  25299  pnt3  25301  ostthlem1  25316  ostth3  25327  axcontlem4  25847  axcontlem9  25852  upgrpredgv  26034  edglnl  26038  numedglnl  26039  usgredg4  26109  nbuhgr2vtx1edgb  26248  wwlksnwwlksnon  26810  2pthon3v  26839  umgr3v3e3cycl  27044  3cyclfrgr  27152  n4cyclfrgr  27155  frgrwopreg  27187  ubthlem3  27728  cdjreui  29291  cdj3i  29300  br8d  29422  xrofsup  29533  xrge0tsmsd  29785  qqhval2  30026  mbfmco2  30327  txpconn  31214  cvmlift2lem10  31294  cvmlift2lem12  31296  cvmlift3lem7  31307  cvmlift3lem8  31308  mclsppslem  31480  br8  31646  br6  31647  br4  31648  noprefixmo  31848  brsegle  32215  tailfb  32372  unbdqndv2  32502  mblfinlem3  33448  ismblfin  33450  itg2addnc  33464  ftc1anc  33493  isbnd2  33582  isbnd3  33583  ssbnd  33587  ispridlc  33869  lshpkrlem6  34402  athgt  34742  3dim1  34753  3dim2  34754  lvolex3N  34824  llncvrlpln2  34843  lplncvrlvol2  34901  linepsubN  35038  lncvrelatN  35067  linepsubclN  35237  eldioph2  37325  eldioph2b  37326  diophin  37336  diophun  37337  fphpdo  37381  irrapxlem3  37388  irrapxlem5  37390  pell1234qrne0  37417  pell1234qrreccl  37418  pell1234qrmulcl  37419  pell14qrgt0  37423  pell14qrdich  37433  pell1qrge1  37434  pell1qrgap  37438  pellqrex  37443  rmxycomplete  37482  jm2.27  37575  stoweidlem49  40266  gbowgt5  41650  m1modmmod  42316