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

Theorem rspcv 3206
Description: Restricted specialization, using implicit substitution. (Contributed by NM, 26-May-1998.)
Hypothesis
Ref Expression
rspcv.1
Assertion
Ref Expression
rspcv
Distinct variable groups:   ,   ,   ,

Proof of Theorem rspcv
StepHypRef Expression
1 nfv 1707 . 2
2 rspcv.1 . 2
31, 2rspc 3204 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  <->wb 184  =wceq 1395  e.wcel 1818  A.wral 2807
This theorem is referenced by:  rspccv  3207  rspcva  3208  rspccva  3209  rspc3v  3222  rr19.3v  3241  rr19.28v  3242  rspsbc  3417  intmin  4306  ralxfrALT  4671  somo  4839  fr2nr  4862  nvocnv  6187  weniso  6250  knatar  6253  grprinvlem  6513  grprinvd  6514  caofref  6566  fr3nr  6615  limuni3  6687  tfinds  6694  funcnvuni  6753  suppfnss  6944  onnseq  7034  smo11  7054  tfrlem1  7064  tfrlem5  7068  tfrlem9  7073  tz7.49  7129  omeulem1  7250  oeordi  7255  nneneq  7720  frfi  7785  unblem2  7793  unbnn2  7797  xpfi  7811  ordiso2  7961  ordtypelem6  7969  ordtypelem7  7970  cantnflem1c  8127  cantnflem1  8129  cantnflem1cOLD  8150  cantnflem1OLD  8152  rankunb  8289  tcrank  8323  carduni  8383  dfac8alem  8431  acni  8447  alephinit  8497  aceq3lem  8522  dfac5  8530  dfac12lem2  8545  dfac12r  8547  dfac12k  8548  pwsdompw  8605  cflm  8651  fin1ai  8694  fin2i  8696  isfin2-2  8720  fin23lem17  8739  fin23lem39  8751  isf32lem1  8754  isf32lem2  8755  isf34lem4  8778  hsmexlem4  8830  axcc3  8839  domtriomlem  8843  axdc3lem2  8852  axdc4lem  8856  axcclem  8858  ttukeylem5  8914  ttukeylem6  8915  axdclem  8920  alephval2  8968  canth4  9046  pwfseqlem5  9062  winainflem  9092  wununi  9105  wunpw  9106  eltskm  9242  dedekind  9765  squeeze0  10473  lbreu  10518  nnsub  10599  ublbneg  11195  zsupss  11200  uzwo3  11206  zmax  11208  zbtwnre  11209  xrub  11532  fzrevral  11792  axdc4uzlem  12092  seqcl2  12125  seqcl  12127  seqf  12128  seqfveq2  12129  seqfveq  12131  seqshft2  12133  monoord  12137  monoord2  12138  sermono  12139  seqsplit  12140  seqcaopr3  12142  seqid  12152  seqid2  12153  seqhomo  12154  seqz  12155  discr1  12302  discr  12303  faclbnd4lem4  12374  hashbclem  12501  wrdind  12702  wrd2ind  12703  reuccats1lem  12705  recan  13169  cau3lem  13187  caubnd2  13190  limsupgre  13304  climi  13333  rlimi  13336  rlimclim1  13368  rlimclim  13369  climrlim2  13370  climshftlem  13397  rlimcld2  13401  rlimcn1  13411  climcn1  13414  subcn2  13417  isercoll  13490  isercoll2  13491  climcau  13493  caucvgrlem  13495  caucvgb  13502  serf0  13503  iseraltlem2  13505  iseraltlem3  13506  iseralt  13507  fsumm1  13566  fsum1p  13568  fsumcom2  13589  fsumge1  13611  telfsumo  13616  telfsumo2  13617  fsumparts  13620  o1fsum  13627  isum1p  13653  isumnn0nn  13654  isumrpcl  13655  climcndslem1  13661  climcndslem2  13662  climcnds  13663  cvgrat  13692  mertenslem1  13693  mertens  13695  clim2prod  13697  ntrivcvgfvn0  13708  fprodm1  13771  fprod1p  13772  fprodcom2  13788  sqrt2irr  13982  ndvdssub  14065  prmind2  14228  nprm  14231  dvdsprm  14240  coprm  14241  pcmpt  14411  pcmpt2  14412  pcmptdvds  14413  pcfac  14418  prmpwdvds  14422  unbenlem  14426  prmreclem4  14437  prmreclem5  14438  vdwlem1  14499  vdwlem2  14500  vdwlem9  14507  vdwlem10  14508  vdwlem13  14511  vdwnnlem1  14513  rami  14533  ramcl  14547  catidex  15071  catideu  15072  iscatd2  15078  catlid  15080  catrid  15081  subcidcl  15213  funcid  15239  yonedalem4c  15546  yonffthlem  15551  isdrs2  15568  lublecllem  15618  lubun  15753  poslubmo  15776  posglbmo  15777  sgrp2rid2ex  16045  grpidd2  16087  mulgsubcl  16156  issubg4  16220  ghmf1  16295  fislw  16645  efgi  16737  efgi2  16743  efgsdmi  16750  efgsrel  16752  gexexlem  16858  gsumzaddlem  16934  gsumzaddlemOLD  16936  gsummhm2  16961  gsummhm2OLD  16962  dprdcntz  17041  dprddisj  17042  dprdss  17076  dprd2dlem2  17089  dprd2da  17091  dpjrid  17111  ablfac1eu  17124  pgpfac1lem1  17125  pgpfaclem2  17133  srgrz  17177  srglz  17178  srgisid  17179  f1rhm0to0ALT  17390  issrngd  17510  islmodd  17518  islmhm2  17684  islbs2  17800  lbsextlem4  17807  rrgeq0i  17937  mvrf1  18081  mplsubglem  18093  mpllsslem  18094  mplsubglemOLD  18095  mpllsslemOLD  18096  subrgasclcl  18164  cply1mul  18335  prmirredlem  18523  prmirredlemOLD  18526  ip2eq  18688  frlmphl  18812  mdetralt  19110  isclo2  19589  lmcvg  19763  cnpnei  19765  iscncl  19770  cncls  19775  lmss  19799  lmff  19802  cnt0  19847  isnrm2  19859  cnrmi  19861  isreg2  19878  cmpcov  19889  tgcmp  19901  uncmp  19903  fiuncmp  19904  bwthOLD  19911  dfcon2  19920  1stcclb  19945  1stcfb  19946  2ndcctbss  19956  1stcelcls  19962  restnlly  19983  islly2  19985  lly1stc  19997  comppfsc  20033  kgeni  20038  kgencn2  20058  ptpjpre1  20072  ptbasfi  20082  ptpjopn  20113  dfac14  20119  txtube  20141  txlm  20149  cnmpt11  20164  cnmpt21  20172  cnmptkp  20181  cnmptk1p  20186  qtopomap  20219  qtopcmap  20220  kqfvima  20231  kqt0lem  20237  isr0  20238  nrmr0reg  20250  fgss2  20375  isufil2  20409  cfinufil  20429  flimopn  20476  fbflim2  20478  flimcf  20483  flfneii  20493  cnpflf  20502  fclssscls  20519  fclsnei  20520  fclsrest  20525  fclscf  20526  flimfnfcls  20529  fclscmp  20531  isfcf  20535  fcfnei  20536  alexsubALTlem3  20549  alexsubALTlem4  20550  alexsubALT  20551  ptcmplem3  20554  tgpt0  20617  tsmsi  20632  tsmsgsum  20637  tsmsgsumOLD  20640  tsmsresOLD  20645  tsmsres  20646  tsmsxplem1  20655  tsmsxplem2  20656  tsmsxp  20657  ustincl  20710  ustdiag  20711  ustinvel  20712  ustexhalf  20713  ucnima  20784  ucncn  20788  cfiluexsm  20793  psmet0  20812  imasdsf1olem  20876  prdsbl  20994  metss  21011  comet  21016  metcnp3  21043  isngp4  21131  nmoi  21235  mulc1cncf  21409  cncfco  21411  cnheiborlem  21454  cnheibor  21455  bndth  21458  lebnumii  21466  nmoleub2lem2  21599  nmoleub3  21602  ipcau2  21677  tchcphlem1  21678  tchcphlem2  21679  lmmcvg  21700  iscfil3  21712  iscau2  21716  iscau4  21718  cmetcaulem  21727  iscmet3lem1  21730  iscmet3lem2  21731  equivcfil  21738  equivcau  21739  lmcau  21751  pjthlem1  21852  pjthlem2  21853  ivthlem1  21863  ivthlem2  21864  ivthlem3  21865  ivth2  21867  ivthle  21868  ivthle2  21869  ivthicc  21870  ovoliunlem1  21913  ovolshftlem1  21920  ovolscalem1  21924  ovolicc2lem3  21930  ovolicc2lem4  21931  ovolicc2  21933  volsup  21966  dyadmbl  22009  vitalilem2  22018  vitalilem3  22019  mbfdm  22035  ismbf  22037  ismbf3d  22061  cncombf  22065  itg2seq  22149  itg2monolem2  22158  itg2monolem3  22159  itg2mono  22160  iblitg  22175  itgconst  22225  itgfsum  22233  limcvallem  22275  ellimc3  22283  cnlimci  22293  cnmptlimc  22294  dvferm1lem  22385  dvferm1  22386  dvferm2lem  22387  dvferm2  22388  dvlipcn  22395  dvle  22408  lhop1lem  22414  lhop1  22415  dvfsumge  22423  dvfsumlem2  22428  dvfsumlem3  22429  dvfsumlem4  22430  dvfsum2  22435  ftc1a  22438  ftc1lem4  22440  itgsubstlem  22449  fta1glem2  22567  fta1g  22568  plyeq0lem  22607  dgrcolem2  22671  dgrco  22672  plydivlem4  22692  plydivex  22693  fta1lem  22703  fta1  22704  vieta1lem2  22707  vieta1  22708  aalioulem2  22729  aalioulem4  22731  tayl0  22757  ulmi  22781  ulmclm  22782  ulmshftlem  22784  ulmcaulem  22789  ulmcau  22790  ulmcn  22794  ulmdvlem1  22795  ulmdvlem3  22797  ulmdv  22798  pserulm  22817  efif1olem4  22932  rlimcnp  23295  rlimcnp2  23296  xrlimcnp  23298  cxploglim  23307  scvxcvx  23315  wilthlem2  23343  ftalem3  23348  fsumdvdscom  23461  musumsum  23468  chtub  23487  fsumvma  23488  perfectlem2  23505  dchrelbas3  23513  dchrelbasd  23514  dchrn0  23525  dchrptlem2  23540  lgsval2lem  23581  lgsdirnn0  23614  lgsdinn0  23615  2sqlem6  23644  2sqlem10  23649  dchrisumlema  23673  dchrisumlem1  23674  dchrisumlem2  23675  dchrisumlem3  23676  dchrmusum2  23679  dchrvmasumlem2  23683  dchrvmasumlem3  23684  dchrvmasumiflem1  23686  dchrisum0flblem2  23694  dchrisum0flb  23695  dchrisum0lem1b  23700  dchrisum0lem2  23703  2vmadivsumlem  23725  chpdifbndlem1  23738  selberg3lem1  23742  selberg4lem1  23745  pntrsumbnd2  23752  pntrlog2bndlem2  23763  pntrlog2bndlem3  23764  pntrlog2bndlem5  23766  pntrlog2bndlem6  23768  pntpbnd1  23771  pntibndlem2  23776  pntibndlem3  23777  pntibnd  23778  pntlemn  23785  pntlemj  23788  pntlemi  23789  pntlemo  23792  pntlem3  23794  pntleml  23796  ostth2lem1  23803  ostth2lem2  23819  ostth3  23823  brbtwn2  24208  colinearalg  24213  axcontlem4  24270  nbgra0nb  24429  nbgrassovt  24435  cusgrarn  24459  usgrasscusgra  24483  wwlknredwwlkn  24726  wwlkextproplem2  24742  clwwlkf1  24796  clwwlkext2edg  24802  clwwisshclwwlem1  24805  clwlkf1clwwlklem  24849  nbhashnn0  24914  rusgraprop4  24944  3cyclfrgrarn1  25012  n4cyclfrgra  25018  frgrawopreglem4  25047  frgrawopreg1  25050  frgrawopreg2  25051  extwwlkfablem2  25078  isgrpo  25198  isgrp2d  25237  opidonOLD  25324  exidu1  25328  rngoideu  25386  blocnilem  25719  ip2eqi  25772  ubthlem1  25786  minvecolem3  25792  htthlem  25834  hial0  26019  hial02  26020  hial2eq  26023  ocorth  26209  occllem  26221  pjhthlem1  26309  h1de2i  26471  pjjsi  26618  lnopunilem1  26929  lnophmlem1  26935  nmcexi  26945  riesz4i  26982  mdi  27214  mdbr3  27216  mdbr4  27217  dmdi  27221  dmdbr3  27224  dmdbr4  27225  dmdi4  27226  mdslmd1i  27248  atss  27265  atom1d  27272  atmd  27318  sumdmdlem2  27338  cdj1i  27352  cdj3i  27360  nn0min  27611  archiabllem1a  27735  archiabllem2a  27738  archiabl  27742  isarchiofld  27807  crefi  27850  pcmplfin  27863  fmcncfil  27913  sigaclcu  28117  unelsiga  28134  measvun  28180  mbfmcnvima  28228  sibfima  28280  lgamgulmlem5  28575  lgambdd  28579  lgamcvglem  28582  derangenlem  28615  subfacp1lem5  28628  subfacp1lem6  28629  rescon  28691  cvmcov  28708  cvmliftlem3  28732  cvmlift2lem10  28757  cvmliftphtlem  28762  mclsax  28929  ghomgrpilem1  29025  ghomf1olem  29034  dfon2lem6  29220  poseq  29333  soseq  29334  nocvxminlem  29450  nobndlem6  29457  fin2so  30040  mbfresfi  30061  ftc1cnnclem  30088  opnrebl2  30139  nn0prpwlem  30140  nn0prpw  30141  neibastop2lem  30178  neibastop2  30179  filnetlem4  30199  seqpo  30240  incsequz  30241  mettrifi  30250  geomcau  30252  caushft  30254  sstotbnd2  30270  equivtotbnd  30274  totbndbnd  30285  ismtybndlem  30302  heibor1lem  30305  bfplem2  30319  isdrngo2  30361  unichnidl  30428  incssnn0  30643  lnmlssfg  31026  unxpwdom3  31041  fnchoice  31404  limcrecl  31635  fourierdlem54  31943  fourierdlem103  31992  fourierdlem104  31993  initoid  32611  termoid  32612  initoeu1  32617  termoeu1  32624  lcosslsp  33039  linindslinci  33049  lindslinindsimp1  33058  ldepsnlinclem1  33106  ldepsnlinclem2  33107  lsat0cv  34758  lcvexchlem4  34762  lcvexchlem5  34763  eqlkr3  34826  lub0N  34914  glb0N  34918  cvrnbtwn  34996  ltrneq2  35872  trlval2  35888  lpolsatN  37215  lpolpolsatN  37216  hdmap14lem12  37609
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