Theorem cbvmptv 4678

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

Step	Hyp	Ref	Expression
1		nfcv 2751	. 2 ⊢ Ⅎ𝑦𝐵
2		nfcv 2751	. 2 ⊢ Ⅎ𝑥𝐶
3		cbvmptv.1	. 2 ⊢ (𝑥 = 𝑦 → 𝐵 = 𝐶)
4	1, 2, 3	cbvmpt 4677	1 ⊢ (𝑥 ∈ 𝐴 ↦ 𝐵) = (𝑦 ∈ 𝐴 ↦ 𝐶)

Syntax hints:   → wi 4   = wceq 1475   ↦ cmpt 4643

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3an 1033  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-rab 2905  df-v 3175  df-dif 3543  df-un 3545  df-in 3547  df-ss 3554  df-nul 3875  df-if 4037  df-sn 4126  df-pr 4128  df-op 4132  df-opab 4644  df-mpt 4645

This theorem is referenced by:  fnmptfvd  6228  onnseq  7328  rdgsucmpt2  7413  frsucmpt2  7422  resixpfo  7832  pw2f1olem  7949  xpmapen  8013  dffi3  8220  ordtypecbv  8305  inf3lema  8404  cantnflem1  8469  cnfcomlem  8479  infxpenc2  8728  fseqenlem1  8730  dfac8a  8736  dfac12r  8851  r1om  8949  fictb  8950  cfsmo  8976  coftr  8978  fin23lem38  9054  compsscnv  9076  isf34lem1  9077  compss  9081  fin1a2lem1  9105  fin1a2lem3  9107  fin1a2lem13  9117  itunisuc  9124  hsmex  9137  domtriom  9148  axdc2  9154  zorn2g  9208  ttukey2g  9221  axdc  9226  konigth  9270  pwcfsdom  9284  canthp1  9355  wunex2  9439  wuncval2  9448  negiso  10880  infrenegsup  10883  rpnnen1  11696  caurcvg2  14256  caucvg  14257  summo  14295  zsum  14296  fsum  14298  ackbijnn  14399  prodmo  14505  zprod  14506  fprod  14510  iprodmul  14573  bpolyval  14619  phimullem  15322  eulerth  15326  iserodd  15378  prmreclem5  15462  prmrec  15464  vdwlem7  15529  vdwlem9  15531  vdwlem10  15532  ramub1  15570  ramcl  15571  yonedalem4c  16740  yonedalem3b  16742  gsumwspan  17206  grplactcnv  17341  galactghm  17646  symgfixfo  17682  pmtrdifwrdel  17728  pmtrdifwrdel2  17729  odf1o2  17811  sylow1lem2  17837  sylow1  17841  sylow2b  17861  sylow3lem1  17865  sylow3lem5  17869  sylow3  17871  efgtf  17958  efgsval  17967  ghmcyg  18120  cycsubgcyg  18125  ablfaclem3  18309  ablfac2  18311  srgbinomlem4  18366  fidomndrnglem  19127  mplmonmul  19285  evlslem2  19333  isphld  19818  frlmphl  19939  mat1ric  20112  mdetralt  20233  smadiadetlem3  20293  pmatcollpw3lem  20407  mp2pm2mplem5  20434  mp2pm2mp  20435  pm2mpmhmlem2  20443  cpmidpmat  20497  cpmadugsumlemF  20500  cpmadugsumfi  20501  cpmadumatpoly  20507  chcoeffeqlem  20509  cayleyhamilton0  20513  cayleyhamilton  20514  cayleyhamiltonALT  20515  cayleyhamilton1  20516  ordtbaslem  20802  ordtbas2  20805  lly1stc  21109  ptpjopn  21225  xkohmeo  21428  fbasrn  21498  elfm  21561  tmdmulg  21706  tmdgsum  21709  qustgpopn  21733  tsmsfbas  21741  tsmsf1o  21758  ustuqtoplem  21853  utopsnneip  21862  fmucnd  21906  ucnextcn  21918  met1stc  22136  prdsxmslem2  22144  metustto  22168  metustexhalf  22171  metuust  22175  cfilucfil2  22176  metuel  22179  metuel2  22180  psmetutop  22182  restmetu  22185  metucn  22186  xrge0tsms  22445  metdsge  22460  expcn  22483  pi1xfrcnv  22665  minveclem3b  23007  minveclem5  23012  minvec  23015  ovollb2  23064  ovolshftlem2  23085  ovolscalem2  23089  ovolicc  23098  ioombl1  23137  uniioombllem6  23162  volsup2  23179  vitali  23188  mbfi1fseq  23294  mbfmullem  23298  itg2seq  23315  itg2i1fseq  23328  itg2addlem  23331  itg2cnlem1  23334  itg2cn  23336  dvfsumrlimge0  23597  plyadd  23777  plymul  23778  coeeu  23785  coeid  23798  dvply2g  23844  plydivex  23856  elqaalem2  23879  elqaa  23881  taylthlem1  23931  taylth  23933  pserval  23968  radcnvlem2  23972  radcnvlt2  23977  dvradcnv  23979  pserulm  23980  psercn  23984  pserdvlem2  23986  pserdv  23987  efgh  24091  eff1olem  24098  circgrp  24102  circsubm  24103  logno1  24182  emcl  24529  harmonicbnd  24530  harmonicbnd2  24531  basel  24616  musum  24717  dchr1  24782  dchrptlem2  24790  dchrpt  24792  lgsqrlem4  24874  lgseisenlem3  24902  2sqlem1  24942  dchrmusumlema  24982  dchrmusum2  24983  dchrvmasumlema  24989  dchrvmasumiflem1  24990  dchrisum0ff  24996  dchrisum0lema  25003  dchrisum0lem1b  25004  dchrisum0lem2a  25006  wlknwwlknvbij  26268  clwlksizeeq  26379  rusgranumwlkg  26485  frgrancvvdeqlemB  26565  frgrancvvdeqlemC  26566  numclwwlk7  26641  ubthlem3  27112  minveco  27124  htth  27159  xrge0tsmsd  29116  madjusmdetlem2  29222  madjusmdet  29225  xrge0mulc1cn  29315  xrge0tmdOLD  29319  xrge0tmd  29320  gsumesum  29448  esumlub  29449  esumpcvgval  29467  esumcvg  29475  esumcvg2  29476  eulerpartlems  29749  eulerpart  29771  fibp1  29790  rrvadd  29841  ballotlemfval  29878  ballotlemi  29889  ballotlemsval  29897  ballotlemsv  29898  ballotlemsf1o  29902  ballotlemrval  29906  ballotlemrinv  29922  signsply0  29954  derangfmla  30426  erdsze  30438  pconpi1  30473  cvmscbv  30494  cvmsss2  30510  cvmliftlem15  30534  cvmlift2  30552  cvmlift3  30564  elmrsubrn  30671  iprodefisum  30880  trpredtr  30974  trpredmintr  30975  knoppcnlem7  31659  knoppf  31696  f1omptsn  32360  mptsnun  32362  fin2so  32566  poimirlem27  32606  broucube  32613  ftc1anclem5  32659  ftc1anclem6  32660  sdclem2  32708  prdstotbnd  32763  prdsbnd2  32764  heiborlem10  32789  lshpkrcl  33421  tendoplcbv  35081  tendo0cbv  35092  tendoicbv  35099  lcfl7N  35808  lcf1o  35858  hdmap1cbv  36110  mzpclval  36306  mzpcompact2lem  36332  rmxyval  36498  dnnumch1  36632  aomclem3  36644  aomclem8  36649  dfac21  36654  pwfi2f1o  36684  dftrcl3  37031  dfrtrcl3  37044  rfovcnvf1od  37318  fsovrfovd  37323  fsovcnvlem  37327  dssmapnvod  37334  clsk3nimkb  37358  radcnvrat  37535  expgrowthi  37554  expgrowth  37556  dvradcnv2  37568  binomcxplemradcnv  37573  binomcxplemdvbinom  37574  binomcxplemdvsum  37576  binomcxplemnotnn0  37577  binomcxp  37578  wessf1ornlem  38366  projf1o  38381  fsumsermpt  38646  fmuldfeqlem1  38649  fprodcn  38667  sumnnodd  38697  fprodsubrecnncnv  38795  fprodaddrecnncnv  38797  dvsinax  38801  fperdvper  38808  dvcosax  38816  ioodvbdlimc1lem1  38821  ioodvbdlimc1  38823  ioodvbdlimc2  38825  dvnmul  38833  dvnprodlem1  38836  dvnprodlem2  38837  dvnprodlem3  38838  dvnprod  38839  itgsin0pilem1  38841  itgiccshift  38872  stoweidlem2  38895  stoweidlem17  38910  stoweidlem32  38925  stoweidlem34  38927  stoweidlem43  38936  stirlinglem2  38968  stirlinglem3  38969  stirlinglem8  38974  dirkerval  38984  dirkerval2  38987  dirkeritg  38995  dirkercncflem3  38998  dirkercncf  39000  fourierdlem14  39014  fourierdlem18  39018  fourierdlem53  39052  fourierdlem62  39061  fourierdlem71  39070  fourierdlem74  39073  fourierdlem75  39074  fourierdlem76  39075  fourierdlem80  39079  fourierdlem81  39080  fourierdlem84  39083  fourierdlem88  39087  fourierdlem92  39091  fourierdlem93  39092  fourierdlem94  39093  fourierdlem95  39094  fourierdlem96  39095  fourierdlem97  39096  fourierdlem98  39097  fourierdlem99  39098  fourierdlem101  39100  fourierdlem103  39102  fourierdlem104  39103  fourierdlem105  39104  fourierdlem106  39105  fourierdlem107  39106  fourierdlem108  39107  fourierdlem110  39109  fourierdlem111  39110  fourierdlem112  39111  fourierdlem113  39112  fourierdlem115  39114  fouriersw  39124  elaa2  39127  etransclem1  39128  etransclem5  39132  etransclem6  39133  etransclem11  39138  etransclem13  39140  etransclem41  39168  etransclem47  39174  etransc  39176  ioorrnopn  39201  ioorrnopnxr  39203  subsaliuncl  39252  sge0resplit  39299  sge0fodjrnlem  39309  nnfoctbdj  39349  iundjiun  39353  voliunsge0lem  39365  meaiuninclem  39373  meaiuninc  39374  meaiininclem  39376  meaiininc  39377  omeiunltfirp  39409  carageniuncllem2  39412  carageniuncl  39413  0ome  39419  isomennd  39421  hoicvrrex  39446  ovn0  39456  ovnsubaddlem2  39461  ovnsubadd  39462  sge0hsphoire  39479  hoidmv1lelem3  39483  hoidmv1le  39484  hoidmvlelem1  39485  hoidmvlelem2  39486  hoidmvlelem3  39487  hoidmvlelem4  39488  hoidmvlelem5  39489  hoidmvle  39490  ovnhoilem2  39492  ovnhoi  39493  hspmbllem2  39517  hspmbl  39519  hoimbl  39521  opnvonmbllem2  39523  ovnsubadd2  39536  ovolval4  39541  ovolval5lem3  39544  ovnovollem3  39548  iccvonmbl  39570  vonioolem2  39572  vonioo  39573  vonicclem2  39575  vonicc  39576  smflimlem4  39660  wlksnwwlknvbij  41114  clwlkssizeeq  41278  frgrncvvdeqlemB  41477  frgrncvvdeqlemC  41478  funcrngcsetcALT  41791  rmsupp0  41943  domnmsuppn0  41944  rmsuppss  41945  suppmptcfin  41954  ply1mulgsum  41972  lcoc0  42005  linc1  42008  lcoel0  42011  lcoss  42019  el0ldep  42049  lincresunit3  42064  isldepslvec2  42068  amgmlemALT  42358