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

Theorem cbvmptv 4672
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 2750 . 2 𝑦𝐵
2 nfcv 2750 . 2 𝑥𝐶
3 cbvmptv.1 . 2 (𝑥 = 𝑦𝐵 = 𝐶)
41, 2, 3cbvmpt 4671 1 (𝑥𝐴𝐵) = (𝑦𝐴𝐶)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1474  cmpt 4637
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-5 1826  ax-6 1874  ax-7 1921  ax-10 2005  ax-11 2020  ax-12 2033  ax-13 2233  ax-ext 2589
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-3an 1032  df-tru 1477  df-ex 1695  df-nf 1700  df-sb 1867  df-clab 2596  df-cleq 2602  df-clel 2605  df-nfc 2739  df-rab 2904  df-v 3174  df-dif 3542  df-un 3544  df-in 3546  df-ss 3553  df-nul 3874  df-if 4036  df-sn 4125  df-pr 4127  df-op 4131  df-opab 4638  df-mpt 4639
This theorem is referenced by:  fnmptfvd  6212  onnseq  7305  rdgsucmpt2  7390  frsucmpt2  7399  resixpfo  7809  pw2f1olem  7926  xpmapen  7990  dffi3  8197  ordtypecbv  8282  inf3lema  8381  cantnflem1  8446  cnfcomlem  8456  infxpenc2  8705  fseqenlem1  8707  dfac8a  8713  dfac12r  8828  r1om  8926  fictb  8927  cfsmo  8953  coftr  8955  fin23lem38  9031  compsscnv  9053  isf34lem1  9054  compss  9058  fin1a2lem1  9082  fin1a2lem3  9084  fin1a2lem13  9094  itunisuc  9101  hsmex  9114  domtriom  9125  axdc2  9131  zorn2g  9185  ttukey2g  9198  axdc  9203  konigth  9247  pwcfsdom  9261  canthp1  9332  wunex2  9416  wuncval2  9425  negiso  10852  infrenegsup  10855  rpnnen1  11654  caurcvg2  14204  caucvg  14205  summo  14243  zsum  14244  fsum  14246  ackbijnn  14347  prodmo  14453  zprod  14454  fprod  14458  iprodmul  14521  bpolyval  14567  phimullem  15270  eulerth  15274  iserodd  15326  prmreclem5  15410  prmrec  15412  vdwlem7  15477  vdwlem9  15479  vdwlem10  15480  ramub1  15518  ramcl  15519  yonedalem4c  16688  yonedalem3b  16690  gsumwspan  17154  grplactcnv  17289  galactghm  17594  symgfixfo  17630  pmtrdifwrdel  17676  pmtrdifwrdel2  17677  odf1o2  17759  sylow1lem2  17785  sylow1  17789  sylow2b  17809  sylow3lem1  17813  sylow3lem5  17817  sylow3  17819  efgtf  17906  efgsval  17915  ghmcyg  18068  cycsubgcyg  18073  ablfaclem3  18257  ablfac2  18259  srgbinomlem4  18314  fidomndrnglem  19075  mplmonmul  19233  evlslem2  19281  isphld  19765  frlmphl  19886  mat1ric  20059  mdetralt  20180  smadiadetlem3  20240  pmatcollpw3lem  20354  mp2pm2mplem5  20381  mp2pm2mp  20382  pm2mpmhmlem2  20390  cpmidpmat  20444  cpmadugsumlemF  20447  cpmadugsumfi  20448  cpmadumatpoly  20454  chcoeffeqlem  20456  cayleyhamilton0  20460  cayleyhamilton  20461  cayleyhamiltonALT  20462  cayleyhamilton1  20463  ordtbaslem  20749  ordtbas2  20752  lly1stc  21056  ptpjopn  21172  xkohmeo  21375  fbasrn  21445  elfm  21508  tmdmulg  21653  tmdgsum  21656  qustgpopn  21680  tsmsfbas  21688  tsmsf1o  21705  ustuqtoplem  21800  utopsnneip  21809  fmucnd  21853  ucnextcn  21865  met1stc  22083  prdsxmslem2  22091  metustto  22115  metustexhalf  22118  metuust  22122  cfilucfil2  22123  metuel  22126  metuel2  22127  psmetutop  22129  restmetu  22132  metucn  22133  xrge0tsms  22392  metdsge  22407  expcn  22430  pi1xfrcnv  22612  minveclem3b  22951  minveclem5  22956  minvec  22959  ovollb2  23008  ovolshftlem2  23029  ovolscalem2  23033  ovolicc  23042  ioombl1  23081  uniioombllem6  23106  volsup2  23123  vitali  23132  mbfi1fseq  23238  mbfmullem  23242  itg2seq  23259  itg2i1fseq  23272  itg2addlem  23275  itg2cnlem1  23278  itg2cn  23280  dvfsumrlimge0  23541  plyadd  23721  plymul  23722  coeeu  23729  coeid  23742  dvply2g  23788  plydivex  23800  elqaalem2  23823  elqaa  23825  taylthlem1  23875  taylth  23877  pserval  23912  radcnvlem2  23916  radcnvlt2  23921  dvradcnv  23923  pserulm  23924  psercn  23928  pserdvlem2  23930  pserdv  23931  efgh  24035  eff1olem  24042  circgrp  24046  circsubm  24047  logno1  24126  emcl  24473  harmonicbnd  24474  harmonicbnd2  24475  basel  24560  musum  24661  dchr1  24726  dchrptlem2  24734  dchrpt  24736  lgsqrlem4  24818  lgseisenlem3  24846  2sqlem1  24886  dchrmusumlema  24926  dchrmusum2  24927  dchrvmasumlema  24933  dchrvmasumiflem1  24934  dchrisum0ff  24940  dchrisum0lema  24947  dchrisum0lem1b  24948  dchrisum0lem2a  24950  wlknwwlknvbij  26061  clwlksizeeq  26172  rusgranumwlkg  26278  frgrancvvdeqlemB  26358  frgrancvvdeqlemC  26359  numclwwlk7  26434  ubthlem3  26905  minveco  26917  htth  26952  xrge0tsmsd  28909  madjusmdetlem2  29015  madjusmdet  29018  xrge0mulc1cn  29108  xrge0tmdOLD  29112  xrge0tmd  29113  gsumesum  29241  esumlub  29242  esumpcvgval  29260  esumcvg  29268  esumcvg2  29269  eulerpartlems  29542  eulerpart  29564  fibp1  29583  rrvadd  29634  ballotlemfval  29671  ballotlemi  29682  ballotlemsval  29690  ballotlemsv  29691  ballotlemsf1o  29695  ballotlemrval  29699  ballotlemrinv  29715  signsply0  29747  derangfmla  30219  erdsze  30231  pconpi1  30266  cvmscbv  30287  cvmsss2  30303  cvmliftlem15  30327  cvmlift2  30345  cvmlift3  30357  elmrsubrn  30464  iprodefisum  30673  trpredtr  30767  trpredmintr  30768  knoppcnlem7  31452  knoppf  31489  f1omptsn  32143  mptsnun  32145  fin2so  32349  poimirlem27  32389  broucube  32396  ftc1anclem5  32442  ftc1anclem6  32443  sdclem2  32491  prdstotbnd  32546  prdsbnd2  32547  heiborlem10  32572  lshpkrcl  33204  tendoplcbv  34864  tendo0cbv  34875  tendoicbv  34882  lcfl7N  35591  lcf1o  35641  hdmap1cbv  35893  mzpclval  36089  mzpcompact2lem  36115  rmxyval  36281  dnnumch1  36415  aomclem3  36427  aomclem8  36432  dfac21  36437  pwfi2f1o  36467  dftrcl3  36814  dfrtrcl3  36827  rfovcnvf1od  37101  fsovrfovd  37106  fsovcnvlem  37110  dssmapnvod  37117  clsk3nimkb  37141  radcnvrat  37318  expgrowthi  37337  expgrowth  37339  dvradcnv2  37351  binomcxplemradcnv  37356  binomcxplemdvbinom  37357  binomcxplemdvsum  37359  binomcxplemnotnn0  37360  binomcxp  37361  wessf1ornlem  38149  projf1o  38164  fsumsermpt  38429  fmuldfeqlem1  38432  fprodcn  38450  sumnnodd  38480  fprodsubrecnncnv  38578  fprodaddrecnncnv  38580  dvsinax  38584  fperdvper  38591  dvcosax  38599  ioodvbdlimc1lem1  38604  ioodvbdlimc1  38606  ioodvbdlimc2  38608  dvnmul  38616  dvnprodlem1  38619  dvnprodlem2  38620  dvnprodlem3  38621  dvnprod  38622  itgsin0pilem1  38624  itgiccshift  38655  stoweidlem2  38678  stoweidlem17  38693  stoweidlem32  38708  stoweidlem34  38710  stoweidlem43  38719  stirlinglem2  38751  stirlinglem3  38752  stirlinglem8  38757  dirkerval  38767  dirkerval2  38770  dirkeritg  38778  dirkercncflem3  38781  dirkercncf  38783  fourierdlem14  38797  fourierdlem18  38801  fourierdlem53  38835  fourierdlem62  38844  fourierdlem71  38853  fourierdlem74  38856  fourierdlem75  38857  fourierdlem76  38858  fourierdlem80  38862  fourierdlem81  38863  fourierdlem84  38866  fourierdlem88  38870  fourierdlem92  38874  fourierdlem93  38875  fourierdlem94  38876  fourierdlem95  38877  fourierdlem96  38878  fourierdlem97  38879  fourierdlem98  38880  fourierdlem99  38881  fourierdlem101  38883  fourierdlem103  38885  fourierdlem104  38886  fourierdlem105  38887  fourierdlem106  38888  fourierdlem107  38889  fourierdlem108  38890  fourierdlem110  38892  fourierdlem111  38893  fourierdlem112  38894  fourierdlem113  38895  fourierdlem115  38897  fouriersw  38907  elaa2  38910  etransclem1  38911  etransclem5  38915  etransclem6  38916  etransclem11  38921  etransclem13  38923  etransclem41  38951  etransclem47  38957  etransc  38959  ioorrnopn  38984  ioorrnopnxr  38986  subsaliuncl  39035  sge0resplit  39082  sge0fodjrnlem  39092  nnfoctbdj  39132  iundjiun  39136  voliunsge0lem  39148  meaiuninclem  39156  meaiuninc  39157  meaiininclem  39159  meaiininc  39160  omeiunltfirp  39192  carageniuncllem2  39195  carageniuncl  39196  0ome  39202  isomennd  39204  hoicvrrex  39229  ovn0  39239  ovnsubaddlem2  39244  ovnsubadd  39245  sge0hsphoire  39262  hoidmv1lelem3  39266  hoidmv1le  39267  hoidmvlelem1  39268  hoidmvlelem2  39269  hoidmvlelem3  39270  hoidmvlelem4  39271  hoidmvlelem5  39272  hoidmvle  39273  ovnhoilem2  39275  ovnhoi  39276  hspmbllem2  39300  hspmbl  39302  hoimbl  39304  opnvonmbllem2  39306  ovnsubadd2  39319  ovolval4  39324  ovolval5lem3  39327  ovnovollem3  39331  iccvonmbl  39353  vonioolem2  39355  vonioo  39356  vonicclem2  39358  vonicc  39359  smflimlem4  39443  wlksnwwlknvbij  41095  clwlkssizeeq  41259  frgrncvvdeqlemB  41458  frgrncvvdeqlemC  41459  funcrngcsetcALT  41772  rmsupp0  41924  domnmsuppn0  41925  rmsuppss  41926  suppmptcfin  41935  ply1mulgsum  41953  lcoc0  41986  linc1  41989  lcoel0  41992  lcoss  42000  el0ldep  42030  lincresunit3  42045  isldepslvec2  42049  amgmlemALT  42300
  Copyright terms: Public domain W3C validator