Theorem rexlimdvva 2962

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

Syntax hints:   -> wi 4   /\ wa 369   e. wcel 1767   E.wrex 2815

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680

This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1597  df-ral 2819  df-rex 2820

This theorem is referenced by:  disjxiun  4444  f1o2ndf1  6891  uniinqs  7391  eroveu  7406  eroprf  7409  ralxpmap  7468  unxpdomlem3  7726  finsschain  7827  dffi3  7891  sornom  8657  genpv  9377  genpdm  9380  1re  9595  cnegex  9760  zaddcl  10903  rexanre  13142  o1lo1  13323  lo1resb  13350  o1resb  13352  rlimcn2  13376  climcn2  13378  o1of2  13398  o1rlimmul  13404  lo1add  13412  lo1mul  13413  summo  13502  o1fsum  13590  dvds2lem  13857  bezoutlem4  14038  dvdsmulgcd  14051  pcqmul  14236  pcneg  14256  pcadd  14267  4sqlem1  14325  4sqlem2  14326  4sqlem4  14329  mul4sq  14331  4sqlem12  14333  4sqlem13  14334  4sqlem18  14339  vdwmc2  14356  vdwlem7  14364  vdwlem9  14366  vdwlem10  14367  vdwlem11  14368  ramlb  14396  ramub1lem2  14404  imasaddfnlem  14783  imasmnd2  15776  imasgrp2  15995  gaorber  16151  psgnunilem2  16326  psgneu  16337  lsmsubm  16479  lsmsubg  16480  lsmmod  16499  lsmdisj2  16506  pj1eu  16520  efgtlen  16550  efgredlem  16571  efgredeu  16576  efgcpbllemb  16579  frgpuptinv  16595  frgpup3lem  16601  divsabl  16674  frgpnabllem1  16680  frgpnabl  16682  cygabl  16696  dprdsubg  16873  ablfacrp  16919  pgpfac1lem3  16930  imasrng  17069  dvdsrtr  17102  lss1d  17409  lsmcl  17529  lsmelval2  17531  lbsextlem2  17605  isnzr2  17710  qsssubdrg  18273  znfld  18394  cygznlem3  18403  psgnghm  18411  lsmcss  18518  mdetunilem7  18915  mdetunilem8  18916  cayleyhamilton0  19185  cayleyhamiltonALT  19187  restbas  19453  ordtbas2  19486  ordtbas  19487  cnhaus  19649  cldllycmp  19790  txbas  19831  ptbasin  19841  txcls  19868  xkoccn  19883  txindis  19898  txlly  19900  txnlly  19901  pthaus  19902  ptrescn  19903  txhaus  19911  tx1stc  19914  txkgen  19916  xkohaus  19917  xkoptsub  19918  xkopt  19919  xkoco1cn  19921  xkoco2cn  19922  xkoinjcn  19951  fmfnfmlem3  20220  fmfnfmlem4  20221  hausflimi  20244  hauspwpwf1  20251  txflf  20270  divstgplem  20382  blin2  20695  prdsxmslem2  20795  xrge0tsms  21102  addcnlem  21131  minveclem3b  21606  pmltpc  21625  evthicc2  21635  dyaddisj  21768  ismbfd  21810  mbfimaopnlem  21825  rolle  22154  dvcnvrelem1  22181  dvcvx  22184  itgsubst  22213  plyf  22358  plypf1  22372  plyadd  22377  plymul  22378  coeeu  22385  dgrlem  22389  coeid  22398  aalioulem6  22495  o1cxp  23060  dchrptlem2  23296  lgsdchr  23379  2sqlem5  23399  2sqlem9  23404  2sqb  23409  pntlemp  23551  pnt3  23553  ostthlem1  23568  ostth3  23579  axcontlem4  23974  axcontlem9  23979  sizeusglecusglem1  24188  el2wlksotot  24586  3cyclfrgra  24719  n4cyclfrgra  24722  frgrawopreg  24754  ubthlem3  25492  cdjreui  27055  cdj3i  27064  br8d  27164  xrofsup  27278  xrge0tsmsd  27466  qqhval2  27627  mbfmco2  27904  txpcon  28345  cvmlift2lem10  28425  cvmlift2lem12  28427  cvmlift3lem7  28438  cvmlift3lem8  28439  ntrivcvgmul  28641  prodmolem2  28672  prodmo  28673  br8  28790  br6  28791  br4  28792  brsegle  29363  mblfinlem3  29658  ismblfin  29660  itg2addnc  29674  ftc1anc  29703  tailfb  29826  isbnd2  29910  isbnd3  29911  ssbnd  29915  ispridlc  30098  eldioph2  30327  eldioph2b  30328  diophin  30338  diophun  30339  fphpdo  30383  irrapxlem3  30392  irrapxlem5  30394  pell1234qrne0  30421  pell1234qrreccl  30422  pell1234qrmulcl  30423  pell14qrgt0  30427  pell14qrdich  30437  pell1qrge1  30438  pell1qrgap  30442  pellqrex  30447  rmxycomplete  30485  jm2.27  30582  stoweidlem49  31377  lshpkrlem6  33930  athgt  34270  3dim1  34281  3dim2  34282  lvolex3N  34352  llncvrlpln2  34371  lplncvrlvol2  34429  linepsubN  34566  lncvrelatN  34595  linepsubclN  34765