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

Theorem rspcva 3208
Description: Restricted specialization, using implicit substitution. (Contributed by NM, 13-Sep-2005.)
Hypothesis
Ref Expression
rspcv.1
Assertion
Ref Expression
rspcva
Distinct variable groups:   ,   ,   ,

Proof of Theorem rspcva
StepHypRef Expression
1 rspcv.1 . . 3
21rspcv 3206 . 2
32imp 429 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  <->wb 184  /\wa 369  =wceq 1395  e.wcel 1818  A.wral 2807
This theorem is referenced by:  rexraleqim  3225  fvn0ssdmfun  6022  fveqdmss  6026  fvcofneq  6039  suppssov1OLD  6532  caofinvl  6567  tfisi  6693  suppssov1  6951  tfrlem1  7064  boxriin  7531  boxcutc  7532  marypha1lem  7913  marypha1  7914  supmo  7932  wemaplem2  7993  unwdomg  8031  noinfepOLD  8098  isinffi  8394  dfac9  8537  sornom  8678  fin23lem11  8718  fin1a2lem13  8813  axdc3lem2  8852  winalim2  9095  grothac  9229  nqereu  9328  infmrcl  10547  nnsub  10599  zextle  10961  xrsupsslem  11527  xrinfmsslem  11528  supxrunb1  11540  supxrunb2  11541  injresinjlem  11925  ssnn0fi  12094  suppssfz  12100  faclbnd4lem4  12374  rexuz3  13181  cau3lem  13187  caubnd2  13190  o1co  13409  climcn1  13414  incexclem  13648  dvdsext  14037  cshwsidrepsw  14578  prdsbasprj  14869  mreintcl  14992  isacs2  15050  acsfiel  15051  isdrs2  15568  lublecllem  15618  joinle  15644  meetle  15658  acsdrsel  15797  isacs4lem  15798  isacs5lem  15799  acsdrscl  15800  acsficl  15801  mgmidmo  15886  gsumval2  15907  mrcmndind  15997  symgfix2  16441  odeq  16574  gexid  16601  mplind  18167  evlslem1  18184  gsummoncoe1  18346  psgndiflemB  18636  mdetunilem1  19114  m2detleiblem3  19131  m2detleiblem4  19132  cpmatmcllem  19219  mp2pm2mplem4  19310  cayleyhamilton1  19393  cmpsublem  19899  cmpsub  19900  hauscmplem  19906  cmpfii  19909  ptpjcn  20112  isufil2  20409  ufileu  20420  isucn2  20782  cfiluweak  20798  cuspcvg  20804  lpbl  21006  lmmbr  21697  caussi  21736  mdeglt  22465  deg1lt  22498  ply1divex  22537  plyco0  22589  dgrco  22672  emcllem7  23331  isppw2  23389  pntleme  23793  pntlemp  23795  tglowdim2ln  24032  nbcusgra  24463  uvtxnbgra  24493  wlkdvspthlem  24609  clwwlkf  24794  rusgranumwlks  24956  frgraunss  24995  vdn0frgrav2  25023  vdgn0frgrav2  25024  vdn1frgrav2  25025  vdgn1frgrav2  25026  frgrancvvdeqlem4  25033  frgraregorufr  25053  extwwlkfablem1  25074  grpoidinvlem3  25208  grpoideu  25211  lnconi  26952  ishashinf  27606  rngurd  27778  tpr2rico  27894  ofcfeqd2  28100  0elsiga  28114  sigaclci  28132  dya2icoseg2  28249  signstfvneq0  28529  derangsn  28614  wfr3g  29342  frr3g  29386  heicant  30049  mblfinlem2  30052  ftc1anc  30098  fdc  30238  bndss  30282  isdrngo2  30361  divrngidl  30425  maxidlmax  30440  ismrcd1  30630  nacsfg  30637  isnacs3  30642  nacsfix  30644  mzpcl1  30661  mzpcl2  30662  mzpcong  30910  dnnumch1  30990  fnwe2lem2  30997  aomclem1  31000  aomclem4  31003  aomclem6  31005  lnr2i  31065  hbtlem5  31077  hbt  31079  islpcn  31645  limclner  31657  cncfshift  31676  cncfperiod  31681  ioodvbdlimc1lem1  31728  ioodvbdlimc1lem2  31729  ioodvbdlimc2lem  31731  fourierdlem103  31992  fourierdlem104  31993  etransclem48  32065  initoeu1  32617  initoeu2  32622  termoeu1  32624  lidldomn1  32727  ply1mulgsumlem2  32987  lindslinindsimp2lem5  33063  lindslinindsimp2  33064  snlindsntor  33072  cdleme0nex  36015  dihglblem2N  37021  hgmapvs  37621
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  ax-6 1747  ax-7 1790  ax-10 1837  ax-11 1842  ax-12 1854  ax-13 1999  ax-ext 2435
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1398  df-ex 1613  df-nf 1617  df-sb 1740  df-clab 2443  df-cleq 2449  df-clel 2452  df-nfc 2607  df-ral 2812  df-v 3111
  Copyright terms: Public domain W3C validator