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

Theorem cbvmptv 4783
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:   𝑥,𝐴   𝑦,𝐴   𝑦,𝐵   𝑥,𝐶
Allowed substitution hints:   𝐵(𝑥)   𝐶(𝑦)

Proof of Theorem cbvmptv
StepHypRef Expression
1 nfcv 2793 . 2 𝑦𝐵
2 nfcv 2793 . 2 𝑥𝐶
3 cbvmptv.1 . 2 (𝑥 = 𝑦𝐵 = 𝐶)
41, 2, 3cbvmpt 4782 1 (𝑥𝐴𝐵) = (𝑦𝐴𝐶)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1523  cmpt 4762
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3an 1056  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-rab 2950  df-v 3233  df-dif 3610  df-un 3612  df-in 3614  df-ss 3621  df-nul 3949  df-if 4120  df-sn 4211  df-pr 4213  df-op 4217  df-opab 4746  df-mpt 4763
This theorem is referenced by:  fnmptfvd  6360  onnseq  7486  rdgsucmpt2  7571  frsucmpt2  7580  resixpfo  7988  pw2f1olem  8105  xpmapen  8169  dffi3  8378  ordtypecbv  8463  inf3lema  8559  cantnflem1  8624  cnfcomlem  8634  infxpenc2  8883  fseqenlem1  8885  dfac8a  8891  dfac12r  9006  r1om  9104  fictb  9105  cfsmo  9131  coftr  9133  fin23lem38  9209  compsscnv  9231  isf34lem1  9232  compss  9236  fin1a2lem1  9260  fin1a2lem3  9262  fin1a2lem13  9272  itunisuc  9279  hsmex  9292  domtriom  9303  axdc2  9309  zorn2g  9363  ttukey2g  9376  axdc  9381  konigth  9429  pwcfsdom  9443  canthp1  9514  wunex2  9598  wuncval2  9607  negiso  11041  infrenegsup  11044  rpnnen1  11858  caurcvg2  14452  caucvg  14453  summo  14492  zsum  14493  fsum  14495  ackbijnn  14604  prodmo  14710  zprod  14711  fprod  14715  iprodmul  14778  bpolyval  14824  phimullem  15531  eulerth  15535  iserodd  15587  prmreclem5  15671  prmrec  15673  vdwlem7  15738  vdwlem9  15740  vdwlem10  15741  ramub1  15779  ramcl  15780  yonedalem4c  16964  yonedalem3b  16966  gsumwspan  17430  grplactcnv  17565  galactghm  17869  symgfixfo  17905  pmtrdifwrdel  17951  pmtrdifwrdel2  17952  odf1o2  18034  sylow1lem2  18060  sylow1  18064  sylow2b  18084  sylow3lem1  18088  sylow3lem5  18092  sylow3  18094  efgtf  18181  efgsval  18190  ghmcyg  18343  cycsubgcyg  18348  ablfaclem3  18532  ablfac2  18534  srgbinomlem4  18589  fidomndrnglem  19354  mplmonmul  19512  evlslem2  19560  isphld  20047  frlmphl  20168  mat1ric  20341  mdetralt  20462  smadiadetlem3  20522  pmatcollpw3lem  20636  mp2pm2mplem5  20663  mp2pm2mp  20664  pm2mpmhmlem2  20672  cpmidpmat  20726  cpmadugsumlemF  20729  cpmadugsumfi  20730  cpmadumatpoly  20736  chcoeffeqlem  20738  cayleyhamilton0  20742  cayleyhamilton  20743  cayleyhamiltonALT  20744  cayleyhamilton1  20745  ordtbaslem  21040  ordtbas2  21043  lly1stc  21347  ptpjopn  21463  xkohmeo  21666  fbasrn  21735  elfm  21798  tmdmulg  21943  tmdgsum  21946  qustgpopn  21970  tsmsfbas  21978  tsmsf1o  21995  ustuqtoplem  22090  utopsnneip  22099  fmucnd  22143  ucnextcn  22155  met1stc  22373  prdsxmslem2  22381  metustto  22405  metustexhalf  22408  metuust  22412  cfilucfil2  22413  metuel  22416  metuel2  22417  psmetutop  22419  restmetu  22422  metucn  22423  xrge0tsms  22684  metdsge  22699  expcn  22722  pi1xfrcnv  22903  minveclem3b  23245  minveclem5  23250  minvec  23253  ovollb2  23303  ovolshftlem2  23324  ovolscalem2  23328  ovolicc  23337  ioombl1  23376  uniioombllem6  23402  volsup2  23419  vitali  23427  mbfi1fseq  23533  mbfmullem  23537  itg2seq  23554  itg2i1fseq  23567  itg2addlem  23570  itg2cnlem1  23573  itg2cn  23575  dvfsumrlimge0  23838  plyadd  24018  plymul  24019  coeeu  24026  coeid  24039  dvply2g  24085  plydivex  24097  elqaalem2  24120  elqaa  24122  taylthlem1  24172  taylth  24174  pserval  24209  radcnvlem2  24213  radcnvlt2  24218  dvradcnv  24220  pserulm  24221  psercn  24225  pserdvlem2  24227  pserdv  24228  efgh  24332  eff1olem  24339  circgrp  24343  circsubm  24344  logno1  24427  emcl  24774  harmonicbnd  24775  harmonicbnd2  24776  basel  24861  musum  24962  dchr1  25027  dchrptlem2  25035  dchrpt  25037  lgsqrlem4  25119  lgseisenlem3  25147  2sqlem1  25187  dchrmusumlema  25227  dchrmusum2  25228  dchrvmasumlema  25234  dchrvmasumiflem1  25235  dchrisum0ff  25241  dchrisum0lema  25248  dchrisum0lem1b  25249  dchrisum0lem2a  25251  wlksnwwlknvbij  26871  clwlkssizeeq  27058  frgrncvvdeqlem8  27286  frgrncvvdeqlem9  27287  ubthlem3  27856  minveco  27868  htth  27903  xrge0tsmsd  29913  madjusmdetlem2  30022  madjusmdet  30025  xrge0mulc1cn  30115  xrge0tmdOLD  30119  xrge0tmd  30120  gsumesum  30249  esumlub  30250  esumpcvgval  30268  esumcvg  30276  esumcvg2  30277  eulerpartlems  30550  eulerpart  30572  fibp1  30591  rrvadd  30642  ballotlemfval  30679  ballotlemi  30690  ballotlemsval  30698  ballotlemsv  30699  ballotlemsf1o  30703  ballotlemrval  30707  ballotlemrinv  30723  signsply0  30756  actfunsnf1o  30810  actfunsnrndisj  30811  itgexpif  30812  hgt750lemb  30862  derangfmla  31298  erdsze  31310  pconnpi1  31345  cvmscbv  31366  cvmsss2  31382  cvmliftlem15  31406  cvmlift2  31424  cvmlift3  31436  elmrsubrn  31543  iprodefisum  31753  trpredtr  31854  trpredmintr  31855  noeta  31993  knoppcnlem7  32614  knoppf  32651  f1omptsn  33314  mptsnun  33316  fin2so  33526  poimirlem27  33566  broucube  33573  ftc1anclem5  33619  ftc1anclem6  33620  sdclem2  33668  prdstotbnd  33723  prdsbnd2  33724  heiborlem10  33749  lshpkrcl  34721  tendoplcbv  36380  tendo0cbv  36391  tendoicbv  36398  lcfl7N  37107  lcf1o  37157  hdmap1cbv  37409  mzpclval  37605  mzpcompact2lem  37631  rmxyval  37797  dnnumch1  37931  aomclem3  37943  aomclem8  37948  dfac21  37953  pwfi2f1o  37983  dftrcl3  38329  dfrtrcl3  38342  rfovcnvf1od  38615  fsovrfovd  38620  fsovcnvlem  38624  dssmapnvod  38631  clsk3nimkb  38655  radcnvrat  38830  expgrowthi  38849  expgrowth  38851  dvradcnv2  38863  binomcxplemradcnv  38868  binomcxplemdvbinom  38869  binomcxplemdvsum  38871  binomcxplemnotnn0  38872  binomcxp  38873  wessf1ornlem  39685  projf1o  39700  fsumsermpt  40129  fmuldfeqlem1  40132  fprodcn  40150  sumnnodd  40180  limsupvaluz  40258  limsupvaluz2  40288  supcnvlimsup  40290  supcnvlimsupmpt  40291  liminfval2  40318  liminflelimsuplem  40325  fprodsubrecnncnv  40440  fprodaddrecnncnv  40442  dvsinax  40445  fperdvper  40451  dvcosax  40459  ioodvbdlimc1lem1  40464  ioodvbdlimc1  40466  ioodvbdlimc2  40468  dvnmul  40476  dvnprodlem1  40479  dvnprodlem2  40480  dvnprodlem3  40481  dvnprod  40482  itgsin0pilem1  40483  itgiccshift  40514  stoweidlem2  40537  stoweidlem17  40552  stoweidlem32  40567  stoweidlem34  40569  stoweidlem43  40578  stirlinglem2  40610  stirlinglem3  40611  stirlinglem8  40616  dirkerval  40626  dirkerval2  40629  dirkeritg  40637  dirkercncflem3  40640  dirkercncf  40642  fourierdlem14  40656  fourierdlem18  40660  fourierdlem53  40694  fourierdlem62  40703  fourierdlem71  40712  fourierdlem74  40715  fourierdlem75  40716  fourierdlem76  40717  fourierdlem80  40721  fourierdlem81  40722  fourierdlem84  40725  fourierdlem88  40729  fourierdlem92  40733  fourierdlem93  40734  fourierdlem94  40735  fourierdlem95  40736  fourierdlem96  40737  fourierdlem97  40738  fourierdlem98  40739  fourierdlem99  40740  fourierdlem101  40742  fourierdlem103  40744  fourierdlem104  40745  fourierdlem105  40746  fourierdlem106  40747  fourierdlem107  40748  fourierdlem108  40749  fourierdlem110  40751  fourierdlem111  40752  fourierdlem112  40753  fourierdlem113  40754  fourierdlem115  40756  fouriersw  40766  elaa2  40769  etransclem1  40770  etransclem5  40774  etransclem6  40775  etransclem11  40780  etransclem13  40782  etransclem41  40810  etransclem47  40816  etransc  40818  ioorrnopn  40843  ioorrnopnxr  40845  subsaliuncl  40894  sge0resplit  40941  sge0fodjrnlem  40951  nnfoctbdj  40991  iundjiun  40995  voliunsge0lem  41007  meaiuninclem  41015  meaiuninc  41016  meaiininclem  41021  meaiininc  41022  omeiunltfirp  41054  carageniuncllem2  41057  carageniuncl  41058  0ome  41064  isomennd  41066  hoicvrrex  41091  ovn0  41101  ovnsubaddlem2  41106  ovnsubadd  41107  sge0hsphoire  41124  hoidmv1lelem3  41128  hoidmv1le  41129  hoidmvlelem1  41130  hoidmvlelem2  41131  hoidmvlelem3  41132  hoidmvlelem4  41133  hoidmvlelem5  41134  hoidmvle  41135  ovnhoilem2  41137  ovnhoi  41138  hspmbllem2  41162  hspmbl  41164  hoimbl  41166  opnvonmbllem2  41168  ovnsubadd2  41181  ovolval4  41186  ovolval5lem3  41189  ovnovollem3  41193  iccvonmbl  41214  vonioolem2  41216  vonioo  41217  vonicclem2  41219  vonicc  41220  smflimlem4  41303  smfsuplem2  41339  smflimsuplem1  41347  smflimsuplem8  41354  smflimsup  41355  funcrngcsetcALT  42324  rmsupp0  42474  domnmsuppn0  42475  rmsuppss  42476  suppmptcfin  42485  ply1mulgsum  42503  lcoc0  42536  linc1  42539  lcoel0  42542  lcoss  42550  el0ldep  42580  lincresunit3  42595  isldepslvec2  42599  amgmlemALT  42877
  Copyright terms: Public domain W3C validator