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

Theorem cbvmptv 4543
Description: Rule to change the bound variable in a maps-to function, using implicit substitution. (Contributed by Mario Carneiro, 19-Feb-2013.)
Hypothesis
Ref Expression
cbvmptv.1
Assertion
Ref Expression
cbvmptv
Distinct variable groups:   ,   ,   ,   ,

Proof of Theorem cbvmptv
StepHypRef Expression
1 nfcv 2619 . 2
2 nfcv 2619 . 2
3 cbvmptv.1 . 2
41, 2, 3cbvmpt 4542 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  =wceq 1395  e.cmpt 4510
This theorem is referenced by:  fnmptfvd  5990  onnseq  7034  rdgsucmpt2  7115  frsucmpt2  7124  resixpfo  7527  pw2f1olem  7641  xpmapen  7705  dffi3  7911  ordtypecbv  7963  inf3lema  8062  cantnflem1  8129  cantnflem1OLD  8152  cnfcomlem  8164  cnfcomlemOLD  8172  infxpenc2  8420  infxpenc2OLD  8424  fseqenlem1  8426  dfac8a  8432  dfac12r  8547  r1om  8645  fictb  8646  cfsmo  8672  coftr  8674  fin23lem38  8750  compsscnv  8772  isf34lem1  8773  compss  8777  fin1a2lem1  8801  fin1a2lem3  8803  fin1a2lem13  8813  itunisuc  8820  hsmex  8833  domtriom  8844  axdc2  8850  zorn2g  8904  ttukey2g  8917  axdc  8922  konigth  8965  pwcfsdom  8979  canthp1  9053  wunex2  9137  wuncval2  9146  negiso  10544  reexALT  11243  caurcvg2  13500  caucvg  13501  summo  13539  zsum  13540  fsum  13542  ackbijnn  13640  prodmo  13743  zprod  13744  fprod  13748  iprodmul  13796  rpnnen  13960  phimullem  14309  eulerth  14313  iserodd  14359  prmreclem5  14438  prmrec  14440  vdwlem7  14505  vdwlem9  14507  vdwlem10  14508  ramub1  14546  ramcl  14547  yonedalem4c  15546  yonedalem3b  15548  gsumwspan  16014  grplactcnv  16138  galactghm  16428  symgfixfo  16464  pmtrdifwrdel  16510  pmtrdifwrdel2  16511  odf1o2  16593  sylow1lem2  16619  sylow1  16623  sylow2b  16643  sylow3lem1  16647  sylow3lem5  16651  sylow3  16653  efgtf  16740  efgsval  16749  ghmcyg  16898  cycsubgcyg  16903  ablfaclem3  17138  ablfac2  17140  srgbinomlem4  17194  fidomndrnglem  17955  mplmonmul  18126  evlslem2  18180  isphld  18689  frlmphl  18812  mat1ric  18989  mdetralt  19110  smadiadetlem3  19170  pmatcollpw3lem  19284  mp2pm2mplem5  19311  mp2pm2mp  19312  pm2mpmhmlem2  19320  cpmidpmat  19374  cpmadugsumlemF  19377  cpmadugsumfi  19378  cpmadumatpoly  19384  chcoeffeqlem  19386  cayleyhamilton0  19390  cayleyhamilton  19391  cayleyhamiltonALT  19392  cayleyhamilton1  19393  ordtbaslem  19689  ordtbas2  19692  lly1stc  19997  ptpjopn  20113  xkohmeo  20316  fbasrn  20385  elfm  20448  tmdmulg  20591  tmdgsum  20594  qustgpopn  20618  tsmsfbas  20626  tsmsf1o  20647  ustuqtoplem  20742  utopsnneip  20751  fmucnd  20795  ucnextcn  20807  met1stc  21024  prdsxmslem2  21032  metusttoOLD  21060  metustto  21061  metustexhalfOLD  21066  metustexhalf  21067  metuustOLD  21074  metuust  21075  cfilucfil2OLD  21076  cfilucfil2  21077  metuelOLD  21080  metuel  21081  metuel2  21082  metutopOLD  21085  psmetutop  21086  restmetu  21090  metucnOLD  21091  metucn  21092  xrge0tsms  21339  metdsge  21353  expcn  21376  pi1xfrcnv  21557  minveclem3b  21843  minveclem5  21848  minvec  21851  ovollb2  21900  ovolshftlem2  21921  ovolscalem2  21925  ovolicc  21934  ioombl1  21972  uniioombllem6  21997  volsup2  22014  vitali  22022  mbfi1fseq  22128  mbfmullem  22132  itg2seq  22149  itg2i1fseq  22162  itg2addlem  22165  itg2cnlem1  22168  itg2cn  22170  dvfsumrlimge0  22431  plyadd  22614  plymul  22615  coeeu  22622  coeid  22635  dvply2g  22681  plydivex  22693  elqaalem2  22716  elqaa  22718  taylthlem1  22768  taylth  22770  pserval  22805  radcnvlem2  22809  radcnvlt2  22814  dvradcnv  22816  pserulm  22817  psercn  22821  pserdvlem2  22823  pserdv  22824  efgh  22928  eff1olem  22935  circgrp  22939  circsubm  22940  logno1  23017  emcl  23332  harmonicbnd  23333  harmonicbnd2  23334  basel  23363  musum  23467  dchr1  23532  dchrptlem2  23540  dchrpt  23542  lgsqrlem4  23619  lgseisenlem3  23626  2sqlem1  23638  dchrmusumlema  23678  dchrmusum2  23679  dchrvmasumlema  23685  dchrvmasumiflem1  23686  dchrisum0ff  23692  dchrisum0lema  23699  dchrisum0lem1b  23700  dchrisum0lem2a  23702  wlknwwlknvbij  24740  clwlksizeeq  24852  rusgranumwlkg  24958  frgrancvvdeqlemB  25038  frgrancvvdeqlemC  25039  numclwwlk7  25114  ubthlem3  25788  minveco  25800  htth  25835  xrge0tsmsd  27775  xrge0mulc1cn  27923  xrge0tmdOLD  27927  xrge0tmd  27928  gsumesum  28067  esumlub  28068  esumpcvgval  28084  esumcvg  28092  esumcvg2  28093  eulerpartlems  28299  eulerpart  28321  fibp1  28340  rrvadd  28391  ballotlemfval  28428  ballotlemi  28439  ballotlemsval  28447  ballotlemsv  28448  ballotlemsf1o  28452  ballotlemrval  28456  ballotlemrinv  28472  signsply0  28508  derangfmla  28634  erdsze  28646  pconpi1  28682  cvmscbv  28703  cvmsss2  28719  cvmliftlem15  28743  cvmlift2  28761  cvmlift3  28773  elmrsubrn  28880  relexpsucr  29053  iprodefisum  29124  trpredtr  29313  trpredmintr  29314  bpolyval  29811  fin2so  30040  ftc1anclem5  30094  ftc1anclem6  30095  sdclem2  30235  prdstotbnd  30290  prdsbnd2  30291  heiborlem10  30316  mzpclval  30657  mzpcompact2lem  30684  rmxyval  30851  dnnumch1  30990  aomclem3  31002  aomclem8  31007  dfac21  31012  pwfi2f1o  31044  radcnvrat  31195  expgrowthi  31238  expgrowth  31240  dvradcnv2  31252  binomcxplemradcnv  31257  binomcxplemdvbinom  31258  binomcxplemdvsum  31260  binomcxplemnotnn0  31261  binomcxp  31262  fmuldfeqlem1  31576  sumnnodd  31636  dvsinax  31708  fperdvper  31715  dvcosax  31723  ioodvbdlimc1lem1  31728  ioodvbdlimc1  31730  ioodvbdlimc2  31732  dvnmul  31740  dvnprodlem1  31743  dvnprodlem2  31744  dvnprodlem3  31745  dvnprod  31746  itgsin0pilem1  31748  itgiccshift  31779  stoweidlem2  31784  stoweidlem17  31799  stoweidlem32  31814  stoweidlem34  31816  stoweidlem43  31825  stirlinglem2  31857  stirlinglem3  31858  stirlinglem8  31863  dirkerval  31873  dirkerval2  31876  dirkeritg  31884  dirkercncflem3  31887  dirkercncf  31889  fourierdlem14  31903  fourierdlem18  31907  fourierdlem53  31942  fourierdlem62  31951  fourierdlem71  31960  fourierdlem74  31963  fourierdlem75  31964  fourierdlem76  31965  fourierdlem80  31969  fourierdlem81  31970  fourierdlem84  31973  fourierdlem88  31977  fourierdlem92  31981  fourierdlem93  31982  fourierdlem94  31983  fourierdlem95  31984  fourierdlem96  31985  fourierdlem97  31986  fourierdlem98  31987  fourierdlem99  31988  fourierdlem101  31990  fourierdlem103  31992  fourierdlem104  31993  fourierdlem105  31994  fourierdlem106  31995  fourierdlem107  31996  fourierdlem108  31997  fourierdlem110  31999  fourierdlem111  32000  fourierdlem112  32001  fourierdlem113  32002  fourierdlem115  32004  fouriersw  32014  elaa2  32017  etransclem1  32018  etransclem5  32022  etransclem6  32023  etransclem11  32028  etransclem13  32030  etransclem41  32058  etransclem47  32064  etransc  32066  usgedgvadf1  32415  usgedgvadf1ALT  32418  funcrngcsetcALT  32807  rmsupp0  32961  domnmsuppn0  32962  rmsuppss  32963  suppmptcfin  32972  ply1mulgsum  32990  lcoc0  33023  linc1  33026  lcoel0  33029  lcoss  33037  el0ldep  33067  lincresunit3  33082  isldepslvec2  33086  lshpkrcl  34841  tendoplcbv  36501  tendo0cbv  36512  tendoicbv  36519  lcfl7N  37228  lcf1o  37278  hdmap1cbv  37530
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-3an 975  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-rab 2816  df-v 3111  df-dif 3478  df-un 3480  df-in 3482  df-ss 3489  df-nul 3785  df-if 3942  df-sn 4030  df-pr 4032  df-op 4036  df-opab 4511  df-mpt 4512
  Copyright terms: Public domain W3C validator