MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  rexlimdva Unicode version

Theorem rexlimdva 2949
Description: Inference from Theorem 19.23 of [Margaris] p. 90 (restricted quantifier version). (Contributed by NM, 20-Jan-2007.)
Hypothesis
Ref Expression
rexlimdva.1
Assertion
Ref Expression
rexlimdva
Distinct variable groups:   ,   ,

Proof of Theorem rexlimdva
StepHypRef Expression
1 rexlimdva.1 . . 3
21ex 434 . 2
32rexlimdv 2947 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  /\wa 369  e.wcel 1818  E.wrex 2808
This theorem is referenced by:  rexlimdvaa  2950  rexlimivv  2954  rexlimdvv  2955  ssexnelpss  3892  ralxfrd  4666  otiunsndisj  4758  foco2  6051  elunirn  6163  f1elima  6171  tfrlem9a  7074  seqomlem2  7135  oawordexr  7224  odi  7247  oelimcl  7268  nnawordex  7305  nnaordex  7306  oaabs  7312  oaabs2  7313  omabs  7315  ectocld  7397  onfin  7728  dif1enOLD  7772  dif1en  7773  isfinite2  7798  isfiniteg  7800  fofinf1o  7821  elfiun  7910  suplub2  7941  supisoex  7953  ordtypelem9  7972  ordtypelem10  7973  brwdom2  8020  brwdom3  8029  rankr1ai  8237  fodomfi2  8462  infpwfien  8464  dfac12r  8547  ackbij1  8639  cff1  8659  fin23lem21  8740  isf32lem2  8755  fin1a2lem11  8811  fin1a2lem13  8813  ficard  8961  pwcfsdom  8979  gchina  9098  eltsk2g  9150  tskr1om2  9167  rankcf  9176  inatsk  9177  tskuni  9182  nqereu  9328  ltexnq  9374  1idpr  9428  suplem1pr  9451  supsrlem  9509  axpre-sup  9567  1re  9616  supmul1  10533  supmul  10536  suprzcl2  11201  qmulz  11214  qbtwnre  11427  ioo0  11583  ico0  11604  ioc0  11605  icc0  11606  fsequb  12085  ssnn0fi  12094  hashdom  12447  reuccats1lem  12705  reuccats1  12706  2cshwcshw  12793  shftlem  12901  rexuzre  13185  rexico  13186  caubnd  13191  limsupbnd1  13305  limsupbnd2  13306  rlim2lt  13320  rlim3  13321  lo1bdd2  13347  lo1bddrp  13348  o1lo1  13360  climuni  13375  climshftlem  13397  o1co  13409  rlimcn1  13411  climcn1  13414  o1rlimmul  13441  lo1le  13474  rlimno1  13476  isercoll  13490  caurcvg2  13500  serf0  13503  summolem2  13538  zsum  13540  fsum2dlem  13585  geomulcvg  13685  mertenslem2  13694  ntrivcvg  13706  zprod  13744  fprod2dlem  13784  dvds1lem  13995  odd2np1lem  14045  odd2np1  14046  dvdssqim  14191  coprmdvds2  14244  isprm5  14253  rpexp  14261  pythagtriplem1  14340  iserodd  14359  pc2dvds  14402  prmpwdvds  14422  4sqlem11  14473  vdwapun  14492  vdwlem2  14500  vdwlem6  14504  vdwlem8  14506  vdwlem10  14508  vdwnnlem1  14513  vdwnnlem3  14515  0ram  14538  ramub1lem2  14545  ramcl  14547  cshwsiun  14584  cshwrepswhash1  14587  firest  14830  imasvscafn  14934  imasmnd2  15957  imasgrp2  16185  issubg4  16220  gaorber  16346  orbsta  16351  pmtr3ncom  16500  psgnran  16540  odmulg  16578  odbezout  16580  gexdvdsi  16603  sylow1lem3  16620  odcau  16624  sylow2alem1  16637  sylow3lem6  16652  lsmelvalm  16671  efgrelexlemb  16768  efgredeu  16770  cyggeninv  16886  cygctb  16894  cyggexb  16901  dprdssv  17056  dprddisj2  17087  dprddisj2OLD  17088  ablfacrplem  17116  pgpfac1lem2  17126  pgpfac1lem5  17130  imasring  17268  dvdsrcl2  17299  dvdsrmul1  17302  lss1d  17609  lssats2  17646  lspsn  17648  lmhmima  17693  lspsneleq  17761  lpiss  17898  mplcoe5lem  18130  mpfind  18205  cply1coe0bi  18342  gsummoncoe1  18346  mpfpf1  18387  pf1mpf  18388  dvdsrzring  18507  dvdsrz  18508  znunit  18602  znrrg  18604  cygznlem3  18608  frgpcyg  18612  psgnghm  18616  psgndif  18638  lindfrn  18856  islinds4  18870  mat1dimelbas  18973  mat1dimcrng  18979  scmatdmat  19017  scmataddcl  19018  scmatsubcl  19019  scmatmulcl  19020  smatvscl  19026  cpmatacl  19217  cpmatinvcl  19218  pmatcollpw3fi1lem2  19288  chpscmat  19343  tgcl  19471  clsval2  19551  neindisj  19618  innei  19626  restcld  19673  restcldr  19675  ordtrest2lem  19704  cnprest  19790  lmss  19799  lmcls  19803  lmcnp  19805  isnrm3  19860  isreg2  19878  cmpcovf  19891  cncmp  19892  cmpsub  19900  1stcrest  19954  2ndcrest  19955  dis2ndc  19961  1stccnp  19963  restnlly  19983  cldllycmp  19996  locfincmp  20027  txcnpi  20109  pthaus  20139  txtube  20141  txcmplem1  20142  txcmplem2  20143  txlm  20149  xkohaus  20154  xkococnlem  20160  xkococn  20161  kqfvima  20231  kqreglem1  20242  isfild  20359  fgcl  20379  filuni  20386  isufil2  20409  ufileu  20420  uffix  20422  rnelfm  20454  fmfnfmlem2  20456  fmfnfmlem4  20458  fmfnfm  20459  fmco  20462  fclsopn  20515  ufilcmp  20533  cnpfcf  20542  alexsublem  20544  alexsubALT  20551  cldsubg  20609  ghmcnp  20613  qustgpopn  20618  tsmsgsum  20637  tsmsgsumOLD  20640  tsmsresOLD  20645  tsmsres  20646  tsmsxplem1  20655  tsmsxp  20657  isucn2  20782  ucnprima  20785  imasdsf1olem  20876  blssps  20927  blss  20928  blssexps  20929  blssex  20930  mopni3  20997  blcld  21008  metrest  21027  metcnp3  21043  reperflem  21323  icccmplem3  21329  xrge0tsms  21339  mulc1cncf  21409  cncfco  21411  cnheibor  21455  bndth  21458  lebnumlem3  21463  xlebnum  21465  lebnumii  21466  nmhmcn  21603  cfil3i  21708  cmetcaulem  21727  cfilres  21735  bcthlem4  21766  bcthlem5  21767  ivthlem2  21864  ivthlem3  21865  ivthicc  21870  cniccbdd  21873  ovolunlem1  21908  ovoliunlem2  21914  ovolshftlem2  21921  ovolicc2  21933  iundisj  21958  iunmbl2  21967  dyadmax  22007  opnmbllem  22010  subopnmbl  22013  volivth  22016  vitalilem2  22018  ismbf3d  22061  mbfimaopn2  22064  mbfaddlem  22067  i1fmullem  22101  mbfi1fseqlem4  22125  ellimc3  22283  dvlip  22394  dvlip2  22396  c1liplem1  22397  dvgt0lem1  22403  dvivthlem2  22410  dvne0  22412  lhop1lem  22414  lhop2  22416  lhop  22417  tdeglem4  22458  mdegnn0cl  22471  ply1divex  22537  dvdsq1p  22561  ig1peu  22572  elply2  22593  plypf1  22609  plydivex  22693  aalioulem3  22730  aalioulem5  22732  aaliou  22734  ulmshftlem  22784  ulmcau  22790  ulmss  22792  ulmbdd  22793  ulmcn  22794  radcnvlt1  22813  eflogeq  22986  efopn  23039  cxpeq  23131  angpieqvd  23162  dcubic  23177  xrlimcnp  23298  cxploglim  23307  ftalem2  23347  ftalem7  23352  isppw2  23389  dchrptlem1  23539  dchrptlem3  23541  dchrsum2  23543  lgsdchrval  23622  lgsdchr  23623  lgsquadlem1  23629  dchrisumlem3  23676  dchrisum0fno1  23696  pntlem3  23794  pntleml  23796  ostth3  23823  brcgr  24203  brbtwn2  24208  axbtwnid  24242  axcontlem7  24273  usgranloop  24379  usgrarnedg1  24389  nbgraf1olem5  24445  wwlkextprop  24744  erclwwlkeqlen  24812  erclwwlktr  24815  clwwlknscsh  24819  erclwwlkneqlen  24824  erclwwlkntr  24827  eleclclwwlkn  24833  hashecclwwlkn1  24834  usghashecclwwlk  24835  el2wlkonot  24869  el2spthonot  24870  el2wlkonotot0  24872  2spontn0vne  24887  vdusgra0nedg  24908  usgravd0nedg  24918  eupai  24967  2pthfrgra  25011  3cyclfrgrarn1  25012  frgraregorufr  25053  frg2wot1  25057  frg2woteq  25060  2spotiundisj  25062  usg2spot2nb  25065  usgreg2spot  25067  2spotmdisj  25068  isgrp2d  25237  ghgrplem1OLD  25368  blocnilem  25719  ubthlem1  25786  ubthlem3  25788  htthlem  25834  shsel3  26233  omlsii  26321  spansncol  26486  nmopun  26933  nmcexi  26945  riesz1  26984  elpjrn  27109  cvcon3  27203  chcv1  27274  atcvatlem  27304  chirredi  27313  br8d  27463  iundisjfi  27601  xrge0tsmsd  27775  ordtrest2NEWlem  27904  lmxrge0  27934  indf1ofs  28039  esumcst  28071  esumfsup  28076  esumpcvgval  28084  measdivcstOLD  28195  eulerpartlemgh  28317  dstfrvunirn  28413  afsval  28551  erdszelem8  28642  erdszelem11  28645  erdsze2lem2  28648  conpcon  28680  sconpi1  28684  cvmsss2  28719  cvmfolem  28724  cvmliftmolem2  28727  cvmliftlem15  28743  cvmlift2lem1  28747  cvmlift3lem4  28767  cvmlift3lem5  28768  mrsub0  28876  mrsubcn  28879  msubrn  28889  msubvrs  28920  dvdspw  29175  br8  29185  br6  29186  br4  29187  trpredtr  29313  frrlem5e  29395  cgrtriv  29652  btwntriv2  29662  btwncomim  29663  btwnswapid  29667  btwnintr  29669  btwnexch3  29670  btwnouttr2  29672  ifscgr  29694  cgrxfr  29705  btwnxfr  29706  btwnconn3  29753  segcon2  29755  brsegle  29758  brsegle2  29759  seglecgr12im  29760  broutsideof3  29776  linethru  29803  elhf2  29832  supaddc  30041  supadd  30042  heicant  30049  opnmbllem0  30050  ismblfin  30055  itg2addnclem  30066  itg2addnclem3  30068  itg2gt0cn  30070  bddiblnc  30085  ftc1anclem5  30094  ftc2nc  30099  opnregcld  30148  cldregopn  30149  neibastop2lem  30178  filbcmb  30231  sdclem1  30236  fdc  30238  incsequz  30241  caushft  30254  istotbnd3  30267  sstotbnd3  30272  equivbnd  30286  cntotbnd  30292  heibor1lem  30305  heibor1  30306  bfplem2  30319  divrngidl  30425  prnc  30464  prtlem10  30606  elrfi  30626  isnacs3  30642  eldiophb  30690  diophrw  30692  eldioph2b  30696  diophin  30706  eldiophss  30708  rexrabdioph  30727  diophren  30747  rencldnfilem  30754  pell1234qrdich  30797  pellfundex  30822  jm2.26a  30942  jm2.27  30950  lsmfgcl  31020  kercvrlsm  31029  lmhmfgima  31030  lpirlnr  31066  hbtlem2  31073  hbtlem4  31075  hbtlem6  31078  rngunsnply  31122  stoweidlem57  31839  stoweidlem61  31843  fourierdlem48  31937  fourierdlem49  31938  otiunsndisjX  32301  ralxfrd2  32303  copisnmnd  32497  lidldomn1  32727  uzlidlring  32735  isldepslvec2  33086  aacllem  33216  lshpdisj  34712  cvrcon3b  35002  atnle  35042  hlhgt2  35113  hl0lt1N  35114  hl2at  35129  cvrexchlem  35143  cvratlem  35145  lvolnlelpln  35309  2lplnj  35344  ispsubcl2N  35671  lautcvr  35816  dva1dim  36711  dib1dim  36892  dib1dim2  36895  diclspsn  36921  dih1dimatlem  37056  dihlatat  37064  dihatexv  37065  dihatexv2  37066  lcfrlem9  37277  lcfrlem16  37285  mapdrvallem2  37372  mapd1o  37375
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
  Copyright terms: Public domain W3C validator