Theorem rexlimdvv 2955

Description: Inference from Theorem 19.23 of [Margaris] p. 90. (Restricted quantifier version.) (Contributed by NM, 22-Jul-2004.)

Hypothesis

Ref	Expression
rexlimdvv.1

Assertion

Ref	Expression
rexlimdvv

Distinct variable groups:   ,,   ,,   ,

Proof of Theorem rexlimdvv

Step	Hyp	Ref	Expression
1		rexlimdvv.1	. . . 4
2	1	expdimp 437	. . 3
3	2	rexlimdv 2947	. 2
4	3	rexlimdva 2949	1

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

This theorem is referenced by:  rexlimdvva  2956  f1oiso2  6248  omeu  7253  xpdom2  7632  elfiun  7910  rankxplim3  8320  brdom6disj  8931  fpwwe2lem12  9040  tskxpss  9171  genpss  9403  genpcd  9405  genpnmax  9406  distrlem1pr  9424  distrlem5pr  9426  ltexprlem6  9440  reclem4pr  9449  supmullem1  10534  supmullem2  10535  qaddcl  11227  qmulcl  11229  sqrlem6  13081  caubnd  13191  summo  13539  xpnnenOLD  13943  bezoutlem3  14178  bezoutlem4  14179  dvdsgcd  14181  gcddiv  14187  pceu  14370  pcqcl  14380  lspfixed  17774  lspexch  17775  lsmcv  17787  lspsolvlem  17788  hausnei2  19854  uncmp  19903  txcnp  20121  tx1stc  20151  fbasrn  20385  rnelfmlem  20453  blssps  20927  blss  20928  tgqioo  21305  ovolunlem2  21909  ax5seg  24241  axpasch  24244  axeuclid  24266  frgrawopreg  25049  pjhthmo  26220  shmodsi  26307  pjpjpre  26337  chscllem4  26558  sumdmdlem  27337  cdj3lem2a  27355  cdj3lem2b  27356  cdj3lem3a  27358  dya2iocnrect  28252  fprb  29203  btwndiff  29677  btwnconn1lem13  29749  btwnconn1lem14  29750  brsegle  29758  segletr  29764  segleantisym  29765  supadd  30042  ismblfin  30055  nn0prpwlem  30140  heibor1lem  30305  crngohomfo  30403  mzpcompact2lem  30684  pellex  30771  mullimc  31622  mullimcf  31629  addlimc  31654  limclner  31657  fourierdlem42  31931  fourierdlem80  31969  fourierdlem97  31986  lsmsat  34733  3dim1  35191  3dim3  35193  1cvratex  35197  atcvrlln2  35243  atcvrlln  35244  lplnnlelln  35267  llncvrlpln2  35281  lplnexllnN  35288  2llnjN  35291  lvolnlelln  35308  lvolnlelpln  35309  lplncvrlvol2  35339  2lplnj  35344  lneq2at  35502  lnatexN  35503  lncvrat  35506  lncmp  35507  paddasslem15  35558  paddasslem16  35559  pmodlem2  35571  pmapjoin  35576  llnexchb2  35593  lhp2lt  35725  cdlemf  36289  cdlemg1cex  36314  cdlemg2ce  36318  cdlemn11pre  36937  dihord2pre  36952  dihord4  36985  dihmeetlem20N  37053  mapdpglem24  37431  mapdpglem32  37432  baerlem3lem2  37437  baerlem5alem2  37438  baerlem5blem2  37439  hdmapglem7  37659

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