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

Theorem cbvrabv 3108
Description: Rule to change the bound variable in a restricted class abstraction, using implicit substitution. (Contributed by NM, 26-May-1999.)
Hypothesis
Ref Expression
cbvrabv.1
Assertion
Ref Expression
cbvrabv
Distinct variable groups:   , ,   ,   ,

Proof of Theorem cbvrabv
StepHypRef Expression
1 nfcv 2619 . 2
2 nfcv 2619 . 2
3 nfv 1707 . 2
4 nfv 1707 . 2
5 cbvrabv.1 . 2
61, 2, 3, 4, 5cbvrab 3107 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  <->wb 184  =wceq 1395  {crab 2811
This theorem is referenced by:  pwnss  4617  knatar  6253  oeeulem  7269  ordtypecbv  7963  ordtypelem9  7972  inf3lema  8062  oemapso  8122  oemapvali  8124  tz9.12lem3  8228  cofsmo  8670  enfin2i  8722  fin23lem33  8746  isf32lem11  8764  zorn2g  8904  pwfseqlem1  9057  pwfseqlem3  9059  zsupss  11200  zmin  11207  reexALT  11243  hashbc  12502  wrd2f1tovbij  12898  sqrlem7  13082  rpnnen  13960  divalglem5  14055  bitsfzolem  14084  smupp1  14130  gcdcllem3  14151  bezout  14180  eulerth  14313  odzval  14318  pcprecl  14363  pcprendvds  14364  pcpremul  14367  pceulem  14369  prmreclem1  14434  prmreclem5  14438  prmreclem6  14439  4sqlem19  14481  vdwnn  14516  hashbcval  14520  gsumvalx  15897  symgfixelq  16458  efgsdm  16748  efgsfo  16757  ablfaclem3  17138  ltbwe  18137  coe1mul2lem2  18309  smadiadetlem3  19170  pptbas  19509  concompss  19934  ptcmplem5  20556  ustuqtop  20749  utopsnneip  20751  icccmplem2  21328  minveclem5  21848  ivth  21866  ovolicc2lem5  21932  ovolicc  21934  opnmbllem  22010  vitali  22022  itg2monolem3  22159  elqaa  22718  radcnvle  22815  pserdvlem2  22823  wilth  23345  ftalem6  23351  ttgval  24178  axcontlem11  24277  nbgraf1olem1  24441  nbgraf1o  24447  cusgraexg  24469  cusgrafi  24482  wlknwwlknbij2  24714  wlkiswwlkbij2  24721  wwlkextbij  24733  wlknwwlknvbij  24740  clwwlkvbij  24801  clwwlknscsh  24819  hashecclwwlkn1  24834  usghashecclwwlk  24835  clwlksizeeq  24852  rusgranumwlklem4  24952  rusgranumwlks  24956  frgraregorufr0  25052  usgreghash2spot  25069  extwwlkfab  25090  numclwwlk5  25112  numclwwlk7  25114  ubthlem3  25788  htth  25835  fcobijfs  27549  locfinreflem  27843  ordtconlem1  27906  ddemeas  28208  oddpwdc  28293  eulerpartgbij  28311  eulerpartlemn  28320  eulerpart  28321  ballotlemelo  28426  ballotleme  28435  ballotlem7  28474  lgamgulmlem5  28575  lgamcvglem  28582  subfacp1lem6  28629  erdsze  28646  cvmscbv  28703  cvmsiota  28722  cvmlift2lem13  28760  mblfinlem1  30051  mblfinlem2  30052  neibastop2  30179  eldioph4i  30746  nzss  31222  limcperiod  31634  cncfshiftioo  31695  ioodvbdlimc1lem2  31729  ioodvbdlimc2lem  31731  dvnprodlem1  31743  dvnprod  31746  itgiccshift  31779  itgperiod  31780  stoweidlem49  31831  fourierdlem41  31930  fourierdlem48  31937  fourierdlem49  31938  fourierdlem54  31943  fourierdlem65  31954  fourierdlem70  31959  fourierdlem71  31960  fourierdlem81  31970  fourierdlem89  31978  fourierdlem90  31979  fourierdlem91  31980  fourierdlem92  31981  fourierdlem96  31985  fourierdlem97  31986  fourierdlem98  31987  fourierdlem99  31988  fourierdlem100  31989  fourierdlem103  31992  fourierdlem104  31993  fourierdlem105  31994  fourierdlem108  31997  fourierdlem109  31998  fourierdlem110  31999  fourierdlem112  32001  fourierdlem113  32002  elaa2  32017  etransclem11  32028  etransc  32066  usgedgleord  32419  usgedgleordALT  32420  lclkrs2  37267
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-or 370  df-an 371  df-ex 1613  df-nf 1617  df-sb 1740  df-clab 2443  df-cleq 2449  df-clel 2452  df-nfc 2607  df-rab 2816
  Copyright terms: Public domain W3C validator