Theorem rexlimdvva 2869

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-10 1775  ax-12 1792

This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1587  df-nf 1590  df-ral 2741  df-rex 2742

This theorem is referenced by:  disjxiun  4310  f1o2ndf1  6701  uniinqs  7201  eroveu  7216  eroprf  7219  ralxpmap  7283  unxpdomlem3  7540  finsschain  7639  dffi3  7702  sornom  8467  genpv  9189  genpdm  9192  1re  9406  cnegex  9571  zaddcl  10706  rexanre  12855  o1lo1  13036  lo1resb  13063  o1resb  13065  rlimcn2  13089  climcn2  13091  o1of2  13111  o1rlimmul  13117  lo1add  13125  lo1mul  13126  summo  13215  o1fsum  13297  dvds2lem  13566  bezoutlem4  13746  dvdsmulgcd  13759  pcqmul  13941  pcneg  13961  pcadd  13972  4sqlem1  14030  4sqlem2  14031  4sqlem4  14034  mul4sq  14036  4sqlem12  14038  4sqlem13  14039  4sqlem18  14044  vdwmc2  14061  vdwlem7  14069  vdwlem9  14071  vdwlem10  14072  vdwlem11  14073  ramlb  14101  ramub1lem2  14109  imasaddfnlem  14487  imasmnd2  15479  imasgrp2  15691  gaorber  15847  psgnunilem2  16022  psgneu  16033  lsmsubm  16173  lsmsubg  16174  lsmmod  16193  lsmdisj2  16200  pj1eu  16214  efgtlen  16244  efgredlem  16265  efgredeu  16270  efgcpbllemb  16273  frgpuptinv  16289  frgpup3lem  16295  divsabl  16368  frgpnabllem1  16372  frgpnabl  16374  cygabl  16388  dprdsubg  16543  ablfacrp  16589  pgpfac1lem3  16600  imasrng  16733  dvdsrtr  16766  lss1d  17066  lsmcl  17186  lsmelval2  17188  lbsextlem2  17262  isnzr2  17367  qsssubdrg  17894  znfld  18015  cygznlem3  18024  psgnghm  18032  lsmcss  18139  mdetunilem7  18446  mdetunilem8  18447  restbas  18784  ordtbas2  18817  ordtbas  18818  cnhaus  18980  cldllycmp  19121  txbas  19162  ptbasin  19172  txcls  19199  xkoccn  19214  txindis  19229  txlly  19231  txnlly  19232  pthaus  19233  ptrescn  19234  txhaus  19242  tx1stc  19245  txkgen  19247  xkohaus  19248  xkoptsub  19249  xkopt  19250  xkoco1cn  19252  xkoco2cn  19253  xkoinjcn  19282  fmfnfmlem3  19551  fmfnfmlem4  19552  hausflimi  19575  hauspwpwf1  19582  txflf  19601  divstgplem  19713  blin2  20026  prdsxmslem2  20126  xrge0tsms  20433  addcnlem  20462  minveclem3b  20937  pmltpc  20956  evthicc2  20966  dyaddisj  21098  ismbfd  21140  mbfimaopnlem  21155  rolle  21484  dvcnvrelem1  21511  dvcvx  21514  itgsubst  21543  plyf  21688  plypf1  21702  plyadd  21707  plymul  21708  coeeu  21715  dgrlem  21719  coeid  21728  aalioulem6  21825  o1cxp  22390  dchrptlem2  22626  lgsdchr  22709  2sqlem5  22729  2sqlem9  22734  2sqb  22739  pntlemp  22881  pnt3  22883  ostthlem1  22898  ostth3  22909  axcontlem4  23235  axcontlem9  23240  sizeusglecusglem1  23414  ubthlem3  24295  cdjreui  25858  cdj3i  25867  br8d  25964  xrofsup  26077  xrge0tsmsd  26275  qqhval2  26433  mbfmco2  26702  txpcon  27143  cvmlift2lem10  27223  cvmlift2lem12  27225  cvmlift3lem7  27236  cvmlift3lem8  27237  ntrivcvgmul  27439  prodmolem2  27470  prodmo  27471  br8  27588  br6  27589  br4  27590  brsegle  28161  mblfinlem3  28456  ismblfin  28458  itg2addnc  28472  ftc1anc  28501  tailfb  28624  isbnd2  28708  isbnd3  28709  ssbnd  28713  ispridlc  28896  eldioph2  29126  eldioph2b  29127  diophin  29137  diophun  29138  fphpdo  29182  irrapxlem3  29191  irrapxlem5  29193  pell1234qrne0  29220  pell1234qrreccl  29221  pell1234qrmulcl  29222  pell14qrgt0  29226  pell14qrdich  29236  pell1qrge1  29237  pell1qrgap  29241  pellqrex  29246  rmxycomplete  29284  jm2.27  29383  stoweidlem49  29870  el2wlksotot  30427  3cyclfrgra  30633  n4cyclfrgra  30636  frgrawopreg  30668  lshpkrlem6  32856  athgt  33196  3dim1  33207  3dim2  33208  lvolex3N  33278  llncvrlpln2  33297  lplncvrlvol2  33355  linepsubN  33492  lncvrelatN  33521  linepsubclN  33691