Theorem cbvmptv 4750

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 2764	. 2 ⊢ Ⅎ𝑦𝐵
2		nfcv 2764	. 2 ⊢ Ⅎ𝑥𝐶
3		cbvmptv.1	. 2 ⊢ (𝑥 = 𝑦 → 𝐵 = 𝐶)
4	1, 2, 3	cbvmpt 4749	1 ⊢ (𝑥 ∈ 𝐴 ↦ 𝐵) = (𝑦 ∈ 𝐴 ↦ 𝐶)

Syntax hints:   → wi 4   = wceq 1483   ↦ cmpt 4729

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1039  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-rab 2921  df-v 3202  df-dif 3577  df-un 3579  df-in 3581  df-ss 3588  df-nul 3916  df-if 4087  df-sn 4178  df-pr 4180  df-op 4184  df-opab 4713  df-mpt 4730

This theorem is referenced by:  fnmptfvd  6320  onnseq  7441  rdgsucmpt2  7526  frsucmpt2  7535  resixpfo  7946  pw2f1olem  8064  xpmapen  8128  dffi3  8337  ordtypecbv  8422  inf3lema  8521  cantnflem1  8586  cnfcomlem  8596  infxpenc2  8845  fseqenlem1  8847  dfac8a  8853  dfac12r  8968  r1om  9066  fictb  9067  cfsmo  9093  coftr  9095  fin23lem38  9171  compsscnv  9193  isf34lem1  9194  compss  9198  fin1a2lem1  9222  fin1a2lem3  9224  fin1a2lem13  9234  itunisuc  9241  hsmex  9254  domtriom  9265  axdc2  9271  zorn2g  9325  ttukey2g  9338  axdc  9343  konigth  9391  pwcfsdom  9405  canthp1  9476  wunex2  9560  wuncval2  9569  negiso  11003  infrenegsup  11006  rpnnen1  11820  caurcvg2  14408  caucvg  14409  summo  14448  zsum  14449  fsum  14451  ackbijnn  14560  prodmo  14666  zprod  14667  fprod  14671  iprodmul  14734  bpolyval  14780  phimullem  15484  eulerth  15488  iserodd  15540  prmreclem5  15624  prmrec  15626  vdwlem7  15691  vdwlem9  15693  vdwlem10  15694  ramub1  15732  ramcl  15733  yonedalem4c  16917  yonedalem3b  16919  gsumwspan  17383  grplactcnv  17518  galactghm  17823  symgfixfo  17859  pmtrdifwrdel  17905  pmtrdifwrdel2  17906  odf1o2  17988  sylow1lem2  18014  sylow1  18018  sylow2b  18038  sylow3lem1  18042  sylow3lem5  18046  sylow3  18048  efgtf  18135  efgsval  18144  ghmcyg  18297  cycsubgcyg  18302  ablfaclem3  18486  ablfac2  18488  srgbinomlem4  18543  fidomndrnglem  19306  mplmonmul  19464  evlslem2  19512  isphld  19999  frlmphl  20120  mat1ric  20293  mdetralt  20414  smadiadetlem3  20474  pmatcollpw3lem  20588  mp2pm2mplem5  20615  mp2pm2mp  20616  pm2mpmhmlem2  20624  cpmidpmat  20678  cpmadugsumlemF  20681  cpmadugsumfi  20682  cpmadumatpoly  20688  chcoeffeqlem  20690  cayleyhamilton0  20694  cayleyhamilton  20695  cayleyhamiltonALT  20696  cayleyhamilton1  20697  ordtbaslem  20992  ordtbas2  20995  lly1stc  21299  ptpjopn  21415  xkohmeo  21618  fbasrn  21688  elfm  21751  tmdmulg  21896  tmdgsum  21899  qustgpopn  21923  tsmsfbas  21931  tsmsf1o  21948  ustuqtoplem  22043  utopsnneip  22052  fmucnd  22096  ucnextcn  22108  met1stc  22326  prdsxmslem2  22334  metustto  22358  metustexhalf  22361  metuust  22365  cfilucfil2  22366  metuel  22369  metuel2  22370  psmetutop  22372  restmetu  22375  metucn  22376  xrge0tsms  22637  metdsge  22652  expcn  22675  pi1xfrcnv  22857  minveclem3b  23199  minveclem5  23204  minvec  23207  ovollb2  23257  ovolshftlem2  23278  ovolscalem2  23282  ovolicc  23291  ioombl1  23330  uniioombllem6  23356  volsup2  23373  vitali  23382  mbfi1fseq  23488  mbfmullem  23492  itg2seq  23509  itg2i1fseq  23522  itg2addlem  23525  itg2cnlem1  23528  itg2cn  23530  dvfsumrlimge0  23793  plyadd  23973  plymul  23974  coeeu  23981  coeid  23994  dvply2g  24040  plydivex  24052  elqaalem2  24075  elqaa  24077  taylthlem1  24127  taylth  24129  pserval  24164  radcnvlem2  24168  radcnvlt2  24173  dvradcnv  24175  pserulm  24176  psercn  24180  pserdvlem2  24182  pserdv  24183  efgh  24287  eff1olem  24294  circgrp  24298  circsubm  24299  logno1  24382  emcl  24729  harmonicbnd  24730  harmonicbnd2  24731  basel  24816  musum  24917  dchr1  24982  dchrptlem2  24990  dchrpt  24992  lgsqrlem4  25074  lgseisenlem3  25102  2sqlem1  25142  dchrmusumlema  25182  dchrmusum2  25183  dchrvmasumlema  25189  dchrvmasumiflem1  25190  dchrisum0ff  25196  dchrisum0lema  25203  dchrisum0lem1b  25204  dchrisum0lem2a  25206  wlksnwwlknvbij  26803  clwlkssizeeq  26971  frgrncvvdeqlem8  27170  frgrncvvdeqlem9  27171  ubthlem3  27728  minveco  27740  htth  27775  xrge0tsmsd  29785  madjusmdetlem2  29894  madjusmdet  29897  xrge0mulc1cn  29987  xrge0tmdOLD  29991  xrge0tmd  29992  gsumesum  30121  esumlub  30122  esumpcvgval  30140  esumcvg  30148  esumcvg2  30149  eulerpartlems  30422  eulerpart  30444  fibp1  30463  rrvadd  30514  ballotlemfval  30551  ballotlemi  30562  ballotlemsval  30570  ballotlemsv  30571  ballotlemsf1o  30575  ballotlemrval  30579  ballotlemrinv  30595  signsply0  30628  actfunsnf1o  30682  actfunsnrndisj  30683  itgexpif  30684  hgt750lemb  30734  derangfmla  31172  erdsze  31184  pconnpi1  31219  cvmscbv  31240  cvmsss2  31256  cvmliftlem15  31280  cvmlift2  31298  cvmlift3  31310  elmrsubrn  31417  iprodefisum  31627  trpredtr  31730  trpredmintr  31731  noeta  31868  knoppcnlem7  32489  knoppf  32526  f1omptsn  33184  mptsnun  33186  fin2so  33396  poimirlem27  33436  broucube  33443  ftc1anclem5  33489  ftc1anclem6  33490  sdclem2  33538  prdstotbnd  33593  prdsbnd2  33594  heiborlem10  33619  lshpkrcl  34403  tendoplcbv  36063  tendo0cbv  36074  tendoicbv  36081  lcfl7N  36790  lcf1o  36840  hdmap1cbv  37092  mzpclval  37288  mzpcompact2lem  37314  rmxyval  37480  dnnumch1  37614  aomclem3  37626  aomclem8  37631  dfac21  37636  pwfi2f1o  37666  dftrcl3  38012  dfrtrcl3  38025  rfovcnvf1od  38298  fsovrfovd  38303  fsovcnvlem  38307  dssmapnvod  38314  clsk3nimkb  38338  radcnvrat  38513  expgrowthi  38532  expgrowth  38534  dvradcnv2  38546  binomcxplemradcnv  38551  binomcxplemdvbinom  38552  binomcxplemdvsum  38554  binomcxplemnotnn0  38555  binomcxp  38556  wessf1ornlem  39371  projf1o  39386  fsumsermpt  39811  fmuldfeqlem1  39814  fprodcn  39832  sumnnodd  39862  limsupvaluz  39940  limsupvaluz2  39970  supcnvlimsup  39972  supcnvlimsupmpt  39973  liminfval2  40000  liminflelimsuplem  40007  fprodsubrecnncnv  40122  fprodaddrecnncnv  40124  dvsinax  40127  fperdvper  40133  dvcosax  40141  ioodvbdlimc1lem1  40146  ioodvbdlimc1  40148  ioodvbdlimc2  40150  dvnmul  40158  dvnprodlem1  40161  dvnprodlem2  40162  dvnprodlem3  40163  dvnprod  40164  itgsin0pilem1  40165  itgiccshift  40196  stoweidlem2  40219  stoweidlem17  40234  stoweidlem32  40249  stoweidlem34  40251  stoweidlem43  40260  stirlinglem2  40292  stirlinglem3  40293  stirlinglem8  40298  dirkerval  40308  dirkerval2  40311  dirkeritg  40319  dirkercncflem3  40322  dirkercncf  40324  fourierdlem14  40338  fourierdlem18  40342  fourierdlem53  40376  fourierdlem62  40385  fourierdlem71  40394  fourierdlem74  40397  fourierdlem75  40398  fourierdlem76  40399  fourierdlem80  40403  fourierdlem81  40404  fourierdlem84  40407  fourierdlem88  40411  fourierdlem92  40415  fourierdlem93  40416  fourierdlem94  40417  fourierdlem95  40418  fourierdlem96  40419  fourierdlem97  40420  fourierdlem98  40421  fourierdlem99  40422  fourierdlem101  40424  fourierdlem103  40426  fourierdlem104  40427  fourierdlem105  40428  fourierdlem106  40429  fourierdlem107  40430  fourierdlem108  40431  fourierdlem110  40433  fourierdlem111  40434  fourierdlem112  40435  fourierdlem113  40436  fourierdlem115  40438  fouriersw  40448  elaa2  40451  etransclem1  40452  etransclem5  40456  etransclem6  40457  etransclem11  40462  etransclem13  40464  etransclem41  40492  etransclem47  40498  etransc  40500  ioorrnopn  40525  ioorrnopnxr  40527  subsaliuncl  40576  sge0resplit  40623  sge0fodjrnlem  40633  nnfoctbdj  40673  iundjiun  40677  voliunsge0lem  40689  meaiuninclem  40697  meaiuninc  40698  meaiininclem  40700  meaiininc  40701  omeiunltfirp  40733  carageniuncllem2  40736  carageniuncl  40737  0ome  40743  isomennd  40745  hoicvrrex  40770  ovn0  40780  ovnsubaddlem2  40785  ovnsubadd  40786  sge0hsphoire  40803  hoidmv1lelem3  40807  hoidmv1le  40808  hoidmvlelem1  40809  hoidmvlelem2  40810  hoidmvlelem3  40811  hoidmvlelem4  40812  hoidmvlelem5  40813  hoidmvle  40814  ovnhoilem2  40816  ovnhoi  40817  hspmbllem2  40841  hspmbl  40843  hoimbl  40845  opnvonmbllem2  40847  ovnsubadd2  40860  ovolval4  40865  ovolval5lem3  40868  ovnovollem3  40872  iccvonmbl  40893  vonioolem2  40895  vonioo  40896  vonicclem2  40898  vonicc  40899  smflimlem4  40982  smfsuplem2  41018  smflimsuplem1  41026  smflimsuplem8  41033  smflimsup  41034  funcrngcsetcALT  41999  rmsupp0  42149  domnmsuppn0  42150  rmsuppss  42151  suppmptcfin  42160  ply1mulgsum  42178  lcoc0  42211  linc1  42214  lcoel0  42217  lcoss  42225  el0ldep  42255  lincresunit3  42270  isldepslvec2  42274  amgmlemALT  42549