Theorem rexlimdvva 2797

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

Syntax hints:   -> wi 4   /\ wa 359   e. wcel 1721   E.wrex 2667

This theorem is referenced by:  disjxiun  4169  f1o2ndf1  6413  uniinqs  6943  eroveu  6958  eroprf  6961  unxpdomlem3  7274  finsschain  7371  dffi3  7394  sornom  8113  genpv  8832  genpdm  8835  1re  9046  cnegex  9203  zaddcl  10273  rexanre  12105  o1lo1  12286  lo1resb  12313  o1resb  12315  rlimcn2  12339  climcn2  12341  o1of2  12361  o1rlimmul  12367  lo1add  12375  lo1mul  12376  summo  12466  o1fsum  12547  dvds2lem  12817  bezoutlem4  12996  dvdsmulgcd  13009  pcqmul  13182  pcneg  13202  pcadd  13213  4sqlem1  13271  4sqlem2  13272  4sqlem4  13275  mul4sq  13277  4sqlem12  13279  4sqlem13  13280  4sqlem18  13285  vdwmc2  13302  vdwlem7  13310  vdwlem9  13312  vdwlem10  13313  vdwlem11  13314  ramlb  13342  ramub1lem2  13350  imasaddfnlem  13708  imasmnd2  14687  imasgrp2  14888  gaorber  15040  lsmsubm  15242  lsmsubg  15243  lsmmod  15262  lsmdisj2  15269  pj1eu  15283  efgtlen  15313  efgredlem  15334  efgredeu  15339  efgcpbllemb  15342  frgpuptinv  15358  frgpup3lem  15364  divsabl  15435  frgpnabllem1  15439  frgpnabl  15441  cygabl  15455  dprdsubg  15537  ablfacrp  15579  pgpfac1lem3  15590  imasrng  15680  dvdsrtr  15712  lss1d  15994  lsmcl  16110  lsmelval2  16112  lbsextlem2  16186  isnzr2  16289  qsssubdrg  16713  znfld  16796  cygznlem3  16805  lsmcss  16874  restbas  17176  ordtbas2  17209  ordtbas  17210  cnhaus  17372  cldllycmp  17511  txbas  17552  ptbasin  17562  txcls  17589  xkoccn  17604  txindis  17619  txlly  17621  txnlly  17622  pthaus  17623  ptrescn  17624  txhaus  17632  tx1stc  17635  txkgen  17637  xkohaus  17638  xkoptsub  17639  xkopt  17640  xkoco1cn  17642  xkoco2cn  17643  xkoinjcn  17672  fmfnfmlem3  17941  fmfnfmlem4  17942  hausflimi  17965  hauspwpwf1  17972  txflf  17991  divstgplem  18103  blin2  18412  prdsxmslem2  18512  xrge0tsms  18818  addcnlem  18847  minveclem3b  19282  pmltpc  19300  evthicc2  19310  dyaddisj  19441  ismbfd  19485  mbfimaopnlem  19500  rolle  19827  dvcnvrelem1  19854  dvcvx  19857  itgsubst  19886  plyf  20070  plypf1  20084  plyadd  20089  plymul  20090  coeeu  20097  dgrlem  20101  coeid  20110  aalioulem6  20207  o1cxp  20766  dchrptlem2  21002  lgsdchr  21085  2sqlem5  21105  2sqlem9  21110  2sqb  21115  pntlemp  21257  pnt3  21259  ostthlem1  21274  ostth3  21285  sizeusglecusglem1  21446  ubthlem3  22327  cdjreui  23888  cdj3i  23897  xrofsup  24079  xrge0tsmsd  24176  qqhval2  24319  mbfmco2  24568  txpcon  24872  cvmlift2lem10  24952  cvmlift2lem12  24954  cvmlift3lem7  24965  cvmlift3lem8  24966  ntrivcvgmul  25183  prodmolem2  25214  prodmo  25215  br8  25327  br6  25328  br4  25329  axcontlem4  25810  axcontlem9  25815  brsegle  25946  mblfinlem2  26144  ismblfin  26146  itg2addnc  26158  tailfb  26296  isbnd2  26382  isbnd3  26383  ssbnd  26387  ispridlc  26570  ralxpmap  26632  eldioph2  26710  eldioph2b  26711  diophin  26721  diophun  26722  fphpdo  26768  irrapxlem3  26777  irrapxlem5  26779  pell1234qrne0  26806  pell1234qrreccl  26807  pell1234qrmulcl  26808  pell14qrgt0  26812  pell14qrdich  26822  pell1qrge1  26823  pell1qrgap  26827  pellqrex  26832  rmxycomplete  26870  jm2.27  26969  psgnunilem2  27286  psgneu  27297  psgnghm  27305  stoweidlem49  27665  el2wlksotot  28079  3cyclfrgra  28119  n4cyclfrgra  28122  frgrawopreg  28152  lshpkrlem6  29598  athgt  29938  3dim1  29949  3dim2  29950  lvolex3N  30020  llncvrlpln2  30039  lplncvrlvol2  30097  linepsubN  30234  lncvrelatN  30263  linepsubclN  30433

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-6 1740  ax-11 1757

This theorem depends on definitions:  df-bi 178  df-an 361  df-ex 1548  df-nf 1551  df-ral 2671  df-rex 2672