Theorem rexlimdvva 2956

Description: Inference from Theorem 19.23 of [Margaris] p. 90. (Restricted quantifier version.) (Contributed by NM, 18-Jun-2014.)

Hypothesis

Ref	Expression
rexlimdvva.1

Assertion

Ref	Expression
rexlimdvva

Distinct variable groups:   ,,   ,,   ,

Proof of Theorem rexlimdvva

Step	Hyp	Ref	Expression
1		rexlimdvva.1	. . 3
2	1	ex 434	. 2
3	2	rexlimdvv 2955	1

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

This theorem is referenced by:  disjxiun  4449  f1o2ndf1  6908  uniinqs  7410  eroveu  7425  eroprf  7428  ralxpmap  7488  unxpdomlem3  7746  finsschain  7847  dffi3  7911  sornom  8678  genpv  9398  genpdm  9401  1re  9616  cnegex  9782  zaddcl  10929  rexanre  13179  o1lo1  13360  lo1resb  13387  o1resb  13389  rlimcn2  13413  climcn2  13415  o1of2  13435  o1rlimmul  13441  lo1add  13449  lo1mul  13450  summo  13539  o1fsum  13627  ntrivcvgmul  13711  prodmolem2  13742  prodmo  13743  dvds2lem  13996  bezoutlem4  14179  dvdsmulgcd  14192  pcqmul  14377  pcneg  14397  pcadd  14408  4sqlem1  14466  4sqlem2  14467  4sqlem4  14470  mul4sq  14472  4sqlem12  14474  4sqlem13  14475  4sqlem18  14480  vdwmc2  14497  vdwlem7  14505  vdwlem9  14507  vdwlem10  14508  vdwlem11  14509  ramlb  14537  ramub1lem2  14545  imasaddfnlem  14925  imasmnd2  15957  imasgrp2  16185  gaorber  16346  psgnunilem2  16520  psgneu  16531  lsmsubm  16673  lsmsubg  16674  lsmmod  16693  lsmdisj2  16700  pj1eu  16714  efgtlen  16744  efgredlem  16765  efgredeu  16770  efgcpbllemb  16773  frgpuptinv  16789  frgpup3lem  16795  qusabl  16871  frgpnabllem1  16877  frgpnabl  16879  cygabl  16893  dprdsubg  17071  ablfacrp  17117  pgpfac1lem3  17128  imasring  17268  dvdsrtr  17301  lss1d  17609  lsmcl  17729  lsmelval2  17731  lbsextlem2  17805  isnzr2  17911  qsssubdrg  18477  znfld  18599  cygznlem3  18608  psgnghm  18616  lsmcss  18723  mdetunilem7  19120  mdetunilem8  19121  cayleyhamilton0  19390  cayleyhamiltonALT  19392  restbas  19659  ordtbas2  19692  ordtbas  19693  cnhaus  19855  cldllycmp  19996  txbas  20068  ptbasin  20078  txcls  20105  xkoccn  20120  txindis  20135  txlly  20137  txnlly  20138  pthaus  20139  ptrescn  20140  txhaus  20148  tx1stc  20151  txkgen  20153  xkohaus  20154  xkoptsub  20155  xkopt  20156  xkoco1cn  20158  xkoco2cn  20159  xkoinjcn  20188  fmfnfmlem3  20457  fmfnfmlem4  20458  hausflimi  20481  hauspwpwf1  20488  txflf  20507  qustgplem  20619  blin2  20932  prdsxmslem2  21032  xrge0tsms  21339  addcnlem  21368  minveclem3b  21843  pmltpc  21862  evthicc2  21872  dyaddisj  22005  ismbfd  22047  mbfimaopnlem  22062  rolle  22391  dvcnvrelem1  22418  dvcvx  22421  itgsubst  22450  plyf  22595  plypf1  22609  plyadd  22614  plymul  22615  coeeu  22622  dgrlem  22626  coeid  22635  aalioulem6  22733  o1cxp  23304  dchrptlem2  23540  lgsdchr  23623  2sqlem5  23643  2sqlem9  23648  2sqb  23653  pntlemp  23795  pnt3  23797  ostthlem1  23812  ostth3  23823  axcontlem4  24270  axcontlem9  24275  sizeusglecusglem1  24484  el2wlksotot  24882  3cyclfrgra  25015  n4cyclfrgra  25018  frgrawopreg  25049  ubthlem3  25788  cdjreui  27351  cdj3i  27360  br8d  27463  xrofsup  27582  xrge0tsmsd  27775  qqhval2  27963  mbfmco2  28236  txpcon  28677  cvmlift2lem10  28757  cvmlift2lem12  28759  cvmlift3lem7  28770  cvmlift3lem8  28771  mclsppslem  28943  br8  29185  br6  29186  br4  29187  brsegle  29758  mblfinlem3  30053  ismblfin  30055  itg2addnc  30069  ftc1anc  30098  tailfb  30195  isbnd2  30279  isbnd3  30280  ssbnd  30284  ispridlc  30467  eldioph2  30695  eldioph2b  30696  diophin  30706  diophun  30707  fphpdo  30751  irrapxlem3  30760  irrapxlem5  30762  pell1234qrne0  30789  pell1234qrreccl  30790  pell1234qrmulcl  30791  pell14qrgt0  30795  pell14qrdich  30805  pell1qrge1  30806  pell1qrgap  30810  pellqrex  30815  rmxycomplete  30853  jm2.27  30950  stoweidlem49  31831  lshpkrlem6  34840  athgt  35180  3dim1  35191  3dim2  35192  lvolex3N  35262  llncvrlpln2  35281  lplncvrlvol2  35339  linepsubN  35476  lncvrelatN  35505  linepsubclN  35675

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704

This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1613  df-ral 2812  df-rex 2813