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

Theorem rspccva 3209
Description: Restricted specialization, using implicit substitution. (Contributed by NM, 26-Jul-2006.) (Proof shortened by Andrew Salmon, 8-Jun-2011.)
Hypothesis
Ref Expression
rspcv.1
Assertion
Ref Expression
rspccva
Distinct variable groups:   ,   ,   ,

Proof of Theorem rspccva
StepHypRef Expression
1 rspcv.1 . . 3
21rspcv 3206 . 2
32impcom 430 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:  disjne  3872  seex  4847  foelrn  6050  fconstfvOLD  6134  grprinvlem  6513  caofid0l  6568  caofid0r  6569  caofid1  6570  caofid2  6571  onnseq  7034  odi  7247  omsmolem  7321  fvixp  7494  unblem1  7792  ordiso2  7961  unwdomg  8031  ac5num  8438  acni2  8448  fodomacn  8458  iundom2g  8936  fpwwe2lem3  9032  eltsk2g  9150  tskpwss  9151  tskpw  9152  tsken  9153  prlem934  9432  dedekindle  9766  ltord1  10104  leord1  10105  eqord1  10106  ltord2  10107  leord2  10108  eqord2  10109  supmul1  10533  seqcaopr2  12143  bccl  12400  hashbc  12502  limsupbnd2  13306  2clim  13395  climsup  13492  caurcvg2  13500  caucvgb  13502  isummulc2  13577  telfsumo2  13617  fsumparts  13620  incexclem  13648  isumshft  13651  climcndslem1  13661  climcndslem2  13662  supcvg  13667  geomulcvg  13685  mertenslem2  13694  mertens  13695  rpnnen2lem10  13957  dvdsprime  14230  iscatd2  15078  fuciso  15344  luble  15617  glble  15630  lubub  15749  lubl  15750  mgmlrid  15893  grpinvex  16065  issubg2  16216  issubg4  16220  nmzbi  16241  gagrpid  16332  cntzi  16367  psgnunilem2  16520  sylow1lem3  16620  pgpfi  16625  slwispgp  16631  sylow2alem1  16637  dprdfcl  17047  dprdfclOLD  17053  ablfac2  17140  abveq0  17475  issrngd  17510  psrbagconf1o  18026  pf1ind  18391  phllmhm  18667  ipcl  18668  ipeq0  18673  isphld  18689  ocvi  18700  cayhamlem3  19388  elcls3  19584  neindisj2  19624  perfi  19656  cnima  19766  1stcfb  19946  1stcelcls  19962  llyi  19975  nllyi  19976  locfinnei  20024  1stckgenlem  20054  ptbasin  20078  txcls  20105  ptcnp  20123  ufli  20415  tgpt0  20617  tsmsxplem2  20656  nrmmetd  21095  tngngp  21168  reperflem  21323  lebnumlem3  21463  htpyi  21474  htpycc  21480  phtpyi  21484  cfili  21707  cmetcvg  21724  caubl  21746  caublcls  21747  bcthlem2  21764  bcthlem3  21765  bcthlem4  21766  ovolicc2lem1  21928  ovolicc2lem5  21932  ovolicc2  21933  voliunlem3  21962  volsuplem  21965  uniioombllem2  21992  mbfima  22039  ismbfd  22047  ismbf3d  22061  mbfmullem  22132  itg2monolem1  22157  itg2i1fseqle  22161  itg2i1fseq  22162  itg2i1fseq2  22163  itg2addlem  22165  bddmulibl  22245  c1liplem1  22397  dvfsumle  22422  dvfsumabs  22424  dvfsumrlimf  22426  dvfsumlem1  22427  dvfsumlem2  22428  dvfsumlem3  22429  dvfsumlem4  22430  dvfsumrlimge0  22431  dvfsum2  22435  ftc1lem6  22442  ulmcau  22790  ulmdvlem1  22795  ulmdvlem3  22797  mtestbdd  22800  itgulm  22803  radcnvlem1  22808  abelthlem5  22830  abelthlem7  22833  areambl  23288  dchrisumlem2  23675  dchrvmasumiflem1  23686  pntpbnd1  23771  ostthlem1  23812  tglowdim1i  23892  brbtwn2  24208  ax5seglem1  24231  ax5seglem2  24232  ax5seglem9  24240  axcontlem4  24270  axcontlem12  24278  usgrcyclnl1  24640  eupaseg  24973  usgreghash2spot  25069  grpoidinvlem3  25208  grpoidinv  25210  grpoidinv2  25220  isgrp2d  25237  cmpidelt  25331  rngoid  25385  vcid  25444  minvecolem5  25797  hcaucvg  26103  hlimconvi  26108  lnopeq0i  26926  cnlnadjlem5  26990  csmdsymi  27253  difelsiga  28133  eulerpartlemb  28307  ballotlemfc0  28431  ballotlemfcc  28432  ptpcon  28678  cvmsdisj  28715  cvmshmeo  28716  snmlflim  28777  elmrsubrn  28880  mvtinf  28915  sinccvg  29039  preddowncl  29276  bpolycl  29814  bpolydif  29817  mblfinlem1  30051  ovoliunnfl  30056  ex-ovoliunnfl  30057  voliunnfl  30058  volsupnfl  30059  mbfresfi  30061  itg2gt0cn  30070  bddiblnc  30085  ftc1cnnc  30089  ftc1anc  30098  fnemeet1  30184  fnemeet2  30185  fnejoin1  30186  fnejoin2  30187  upixp  30220  filbcmb  30231  sdclem1  30236  seqpo  30240  incsequz2  30242  mettrifi  30250  caushft  30254  sstotbnd2  30270  heibor1lem  30305  heiborlem3  30309  heiborlem10  30316  heibor  30317  rrndstprj2  30327  limsuc2  30986  cvgdvgrat  31194  cncmpmax  31407  mccllem  31605  mccl  31606  climinf  31612  climsuse  31614  islptre  31625  limcperiod  31634  addlimc  31654  0ellimcdiv  31655  cncficcgt0  31691  fperdvper  31715  dvbdfbdioolem2  31726  ioodvbdlimc1lem2  31729  ioodvbdlimc2lem  31731  dvnprodlem3  31745  stoweidlem7  31789  stoweidlem15  31797  stoweidlem21  31803  stoweidlem31  31813  stoweidlem35  31817  stoweidlem36  31818  stoweidlem50  31832  stoweidlem57  31839  stoweidlem59  31841  wallispilem3  31849  dirkercncflem2  31886  dirkercncflem4  31888  fourierdlem32  31921  fourierdlem33  31922  fourierdlem39  31928  fourierdlem62  31951  fourierdlem71  31960  fourierdlem89  31978  fourierdlem91  31980  fourierdlem93  31982  fourierdlem101  31990  fourierdlem103  31992  fourierdlem104  31993  etransclem24  32041  etransclem32  32049  bj-seex  34491
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