Theorem rexlimdvva 2838

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 2837	1 |- ( ph -> ( E. x e. A E. y e. B ps -> ch ) )

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1594  ax-4 1605  ax-5 1669  ax-6 1707  ax-7 1727  ax-10 1774  ax-12 1791

This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1590  df-nf 1593  df-ral 2710  df-rex 2711

This theorem is referenced by:  disjxiun  4277  f1o2ndf1  6669  uniinqs  7168  eroveu  7183  eroprf  7186  ralxpmap  7250  unxpdomlem3  7507  finsschain  7606  dffi3  7669  sornom  8434  genpv  9155  genpdm  9158  1re  9372  cnegex  9537  zaddcl  10672  rexanre  12817  o1lo1  12998  lo1resb  13025  o1resb  13027  rlimcn2  13051  climcn2  13053  o1of2  13073  o1rlimmul  13079  lo1add  13087  lo1mul  13088  summo  13177  o1fsum  13258  dvds2lem  13527  bezoutlem4  13707  dvdsmulgcd  13720  pcqmul  13902  pcneg  13922  pcadd  13933  4sqlem1  13991  4sqlem2  13992  4sqlem4  13995  mul4sq  13997  4sqlem12  13999  4sqlem13  14000  4sqlem18  14005  vdwmc2  14022  vdwlem7  14030  vdwlem9  14032  vdwlem10  14033  vdwlem11  14034  ramlb  14062  ramub1lem2  14070  imasaddfnlem  14448  imasmnd2  15440  imasgrp2  15649  gaorber  15805  psgnunilem2  15980  psgneu  15991  lsmsubm  16131  lsmsubg  16132  lsmmod  16151  lsmdisj2  16158  pj1eu  16172  efgtlen  16202  efgredlem  16223  efgredeu  16228  efgcpbllemb  16231  frgpuptinv  16247  frgpup3lem  16253  divsabl  16326  frgpnabllem1  16330  frgpnabl  16332  cygabl  16346  dprdsubg  16494  ablfacrp  16540  pgpfac1lem3  16551  imasrng  16645  dvdsrtr  16677  lss1d  16965  lsmcl  17085  lsmelval2  17087  lbsextlem2  17161  isnzr2  17266  qsssubdrg  17715  znfld  17834  cygznlem3  17843  psgnghm  17851  lsmcss  17958  mdetunilem7  18265  mdetunilem8  18266  restbas  18603  ordtbas2  18636  ordtbas  18637  cnhaus  18799  cldllycmp  18940  txbas  18981  ptbasin  18991  txcls  19018  xkoccn  19033  txindis  19048  txlly  19050  txnlly  19051  pthaus  19052  ptrescn  19053  txhaus  19061  tx1stc  19064  txkgen  19066  xkohaus  19067  xkoptsub  19068  xkopt  19069  xkoco1cn  19071  xkoco2cn  19072  xkoinjcn  19101  fmfnfmlem3  19370  fmfnfmlem4  19371  hausflimi  19394  hauspwpwf1  19401  txflf  19420  divstgplem  19532  blin2  19845  prdsxmslem2  19945  xrge0tsms  20252  addcnlem  20281  minveclem3b  20756  pmltpc  20775  evthicc2  20785  dyaddisj  20917  ismbfd  20959  mbfimaopnlem  20974  rolle  21303  dvcnvrelem1  21330  dvcvx  21333  itgsubst  21362  plyf  21550  plypf1  21564  plyadd  21569  plymul  21570  coeeu  21577  dgrlem  21581  coeid  21590  aalioulem6  21687  o1cxp  22252  dchrptlem2  22488  lgsdchr  22571  2sqlem5  22591  2sqlem9  22596  2sqb  22601  pntlemp  22743  pnt3  22745  ostthlem1  22760  ostth3  22771  axcontlem4  23035  axcontlem9  23040  sizeusglecusglem1  23214  ubthlem3  24095  cdjreui  25658  cdj3i  25667  br8d  25765  xrofsup  25877  xrge0tsmsd  26105  qqhval2  26264  mbfmco2  26533  txpcon  26968  cvmlift2lem10  27048  cvmlift2lem12  27050  cvmlift3lem7  27061  cvmlift3lem8  27062  ntrivcvgmul  27263  prodmolem2  27294  prodmo  27295  br8  27412  br6  27413  br4  27414  brsegle  27985  mblfinlem3  28271  ismblfin  28273  itg2addnc  28287  ftc1anc  28316  tailfb  28439  isbnd2  28523  isbnd3  28524  ssbnd  28528  ispridlc  28711  eldioph2  28942  eldioph2b  28943  diophin  28953  diophun  28954  fphpdo  28998  irrapxlem3  29007  irrapxlem5  29009  pell1234qrne0  29036  pell1234qrreccl  29037  pell1234qrmulcl  29038  pell14qrgt0  29042  pell14qrdich  29052  pell1qrge1  29053  pell1qrgap  29057  pellqrex  29062  rmxycomplete  29100  jm2.27  29199  stoweidlem49  29687  el2wlksotot  30244  3cyclfrgra  30450  n4cyclfrgra  30453  frgrawopreg  30485  lshpkrlem6  32330  athgt  32670  3dim1  32681  3dim2  32682  lvolex3N  32752  llncvrlpln2  32771  lplncvrlvol2  32829  linepsubN  32966  lncvrelatN  32995  linepsubclN  33165