Theorem cbvmptv 5133

Description: Rule to change the bound variable in a maps-to function, using implicit substitution. (Contributed by Mario Carneiro, 19-Feb-2013.) Add disjoint variable condition to avoid ax-13 2379. See cbvmptvg 5134 for a less restrictive version requiring more axioms. (Revised by Gino Giotto, 17-Jan-2024.)

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

Syntax hints:   → wi 4   = wceq 1538   ↦ cmpt 5110

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2158  ax-12 2175  ax-ext 2770

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-clab 2777  df-cleq 2791  df-clel 2870  df-nfc 2938  df-v 3443  df-un 3886  df-sn 4526  df-pr 4528  df-op 4532  df-opab 5093  df-mpt 5111

This theorem is referenced by:  fnmptfvd  6788  onnseq  7964  rdgsucmpt2  8049  frsucmpt2w  8058  frsucmpt2  8059  resixpfo  8483  pw2f1olem  8604  xpmapen  8669  dffi3  8879  ordtypecbv  8965  inf3lema  9071  cantnflem1  9136  cnfcomlem  9146  infxpenc2  9433  fseqenlem1  9435  dfac8a  9441  dfac12r  9557  r1om  9655  fictb  9656  cfsmo  9682  coftr  9684  fin23lem38  9760  compsscnv  9782  isf34lem1  9783  compss  9787  fin1a2lem1  9811  fin1a2lem3  9813  fin1a2lem13  9823  itunisuc  9830  hsmex  9843  domtriom  9854  axdc2  9860  zorn2g  9914  ttukey2g  9927  axdc  9932  konigth  9980  pwcfsdom  9994  canthp1  10065  wunex2  10149  wuncval2  10158  negiso  11608  infrenegsup  11611  rpnnen1  12370  caurcvg2  15026  caucvg  15027  summo  15066  zsum  15067  fsum  15069  ackbijnn  15175  prodmo  15282  zprod  15283  fprod  15287  iprodmul  15349  bpolyval  15395  phimullem  16106  eulerth  16110  iserodd  16162  prmreclem5  16246  prmrec  16248  vdwlem7  16313  vdwlem9  16315  vdwlem10  16316  ramub1  16354  ramcl  16355  yonedalem4c  17519  yonedalem3b  17521  gsumwspan  18003  smndex1iidm  18058  smndex1gid  18060  smndex2dlinvh  18074  grplactcnv  18194  galactghm  18524  symgfixfo  18559  pmtrdifwrdel  18605  pmtrdifwrdel2  18606  odf1o2  18690  sylow1lem2  18716  sylow1  18720  sylow2b  18740  sylow3lem1  18744  sylow3lem5  18748  sylow3  18750  efgtf  18840  efgsval  18849  ghmcyg  19009  cycsubgcyg  19014  ablfaclem3  19202  ablfac2  19204  srgbinomlem4  19286  fidomndrnglem  20072  isphld  20343  frlmphl  20470  mplmonmul  20704  evlslem2  20751  mat1ric  21092  mdetralt  21213  smadiadetlem3  21273  pmatcollpw3lem  21388  mp2pm2mplem5  21415  mp2pm2mp  21416  pm2mpmhmlem2  21424  cpmidpmat  21478  cpmadugsumlemF  21481  cpmadugsumfi  21482  cpmadumatpoly  21488  chcoeffeqlem  21490  cayleyhamilton0  21494  cayleyhamilton  21495  cayleyhamiltonALT  21496  cayleyhamilton1  21497  ordtbaslem  21793  ordtbas2  21796  lly1stc  22101  ptpjopn  22217  xkohmeo  22420  fbasrn  22489  elfm  22552  tmdmulg  22697  tmdgsum  22700  qustgpopn  22725  tsmsfbas  22733  tsmsf1o  22750  ustuqtoplem  22845  utopsnneip  22854  fmucnd  22898  ucnextcn  22910  met1stc  23128  prdsxmslem2  23136  metustto  23160  metustexhalf  23163  metuust  23167  cfilucfil2  23168  metuel  23171  metuel2  23172  psmetutop  23174  restmetu  23177  metucn  23178  xrge0tsms  23439  metdsge  23454  expcn  23477  pi1xfrcnv  23662  minveclem3b  24032  minveclem5  24037  minvec  24040  ovollb2  24093  ovolshftlem2  24114  ovolscalem2  24118  ovolicc  24127  ioombl1  24166  uniioombllem6  24192  volsup2  24209  vitali  24217  mbfi1fseq  24325  mbfmullem  24329  itg2seq  24346  itg2i1fseq  24359  itg2addlem  24362  itg2cnlem1  24365  itg2cn  24367  dvfsumrlimge0  24633  plyadd  24814  plymul  24815  coeeu  24822  coeid  24835  dvply2g  24881  plydivex  24893  elqaalem2  24916  elqaa  24918  taylthlem1  24968  taylth  24970  pserval  25005  radcnvlem2  25009  radcnvlt2  25014  dvradcnv  25016  pserulm  25017  psercn  25021  pserdvlem2  25023  pserdv  25024  efgh  25133  eff1olem  25140  circgrp  25144  circsubm  25145  logno1  25227  emcl  25588  harmonicbnd  25589  harmonicbnd2  25590  basel  25675  musum  25776  dchr1  25841  dchrptlem2  25849  dchrpt  25851  lgsqrlem4  25933  lgseisenlem3  25961  2sqlem1  26001  dchrmusumlema  26077  dchrmusum2  26078  dchrvmasumlema  26084  dchrvmasumiflem1  26085  dchrisum0ff  26091  dchrisum0lema  26098  dchrisum0lem1b  26099  dchrisum0lem2a  26101  wlknwwlksnbij  27674  clwlkclwwlken  27797  clwlknf1oclwwlkn  27869  frgrncvvdeqlem8  28091  frgrncvvdeqlem9  28092  numclwwlk1lem2  28145  ubthlem3  28655  minveco  28667  htth  28701  fsuppcurry1  30487  fsuppcurry2  30488  gsumhashmul  30741  xrge0tsmsd  30742  elrspunidl  31014  lbsdiflsp0  31110  fedgmullem1  31113  fedgmul  31115  madjusmdetlem2  31181  madjusmdet  31184  zartop  31229  zartopon  31230  zart0  31232  zarmxt1  31233  zarcmp  31235  rhmpreimacn  31238  xrge0mulc1cn  31294  xrge0tmd  31298  xrge0tmdALT  31299  gsumesum  31428  esumlub  31429  esumpcvgval  31447  esumcvg  31455  esumcvg2  31456  eulerpartlems  31728  eulerpart  31750  fibp1  31769  rrvadd  31820  ballotlemfval  31857  ballotlemi  31868  ballotlemsval  31876  ballotlemsv  31877  ballotlemsf1o  31881  ballotlemrval  31885  ballotlemrinv  31901  signsply0  31931  actfunsnf1o  31985  actfunsnrndisj  31986  itgexpif  31987  hgt750lemb  32037  derangfmla  32550  erdsze  32562  pconnpi1  32597  cvmscbv  32618  cvmsss2  32634  cvmliftlem15  32658  cvmlift2  32676  cvmlift3  32688  elmrsubrn  32880  iprodefisum  33086  trpredtr  33182  trpredmintr  33183  noeta  33335  knoppcnlem7  33951  knoppf  33987  f1omptsn  34754  mptsnun  34756  fin2so  35044  poimirlem27  35084  broucube  35091  ftc1anclem5  35134  ftc1anclem6  35135  sdclem2  35180  prdstotbnd  35232  prdsbnd2  35233  heiborlem10  35258  lshpkrcl  36412  tendoplcbv  38071  tendo0cbv  38082  tendoicbv  38089  lcfl7N  38797  lcf1o  38847  hdmap1cbv  39098  frlmsnic  39453  mzpclval  39666  mzpcompact2lem  39692  rmxyval  39856  dnnumch1  39988  aomclem3  40000  aomclem8  40005  dfac21  40010  pwfi2f1o  40040  dftrcl3  40421  dfrtrcl3  40434  rfovcnvf1od  40705  fsovrfovd  40710  fsovcnvlem  40714  dssmapnvod  40721  clsk3nimkb  40743  radcnvrat  41018  expgrowthi  41037  expgrowth  41039  dvradcnv2  41051  binomcxplemradcnv  41056  binomcxplemdvbinom  41057  binomcxplemdvsum  41059  binomcxplemnotnn0  41060  binomcxp  41061  wessf1ornlem  41811  projf1o  41825  fsumsermpt  42221  fmuldfeqlem1  42224  fprodcn  42242  sumnnodd  42272  limsupvaluz  42350  limsupvaluz2  42380  supcnvlimsup  42382  supcnvlimsupmpt  42383  liminfval2  42410  liminflelimsuplem  42417  fprodsubrecnncnv  42550  fprodaddrecnncnv  42552  dvsinax  42555  fperdvper  42561  dvcosax  42568  ioodvbdlimc1lem1  42573  ioodvbdlimc1  42575  ioodvbdlimc2  42577  dvnmul  42585  dvnprodlem1  42588  dvnprodlem2  42589  dvnprodlem3  42590  dvnprod  42591  itgsin0pilem1  42592  itgiccshift  42622  stoweidlem2  42644  stoweidlem17  42659  stoweidlem32  42674  stoweidlem34  42676  stoweidlem43  42685  stirlinglem2  42717  stirlinglem3  42718  stirlinglem8  42723  dirkerval  42733  dirkerval2  42736  dirkeritg  42744  dirkercncflem3  42747  dirkercncf  42749  fourierdlem14  42763  fourierdlem18  42767  fourierdlem53  42801  fourierdlem62  42810  fourierdlem71  42819  fourierdlem74  42822  fourierdlem75  42823  fourierdlem76  42824  fourierdlem80  42828  fourierdlem81  42829  fourierdlem84  42832  fourierdlem88  42836  fourierdlem92  42840  fourierdlem93  42841  fourierdlem94  42842  fourierdlem95  42843  fourierdlem96  42844  fourierdlem97  42845  fourierdlem98  42846  fourierdlem99  42847  fourierdlem101  42849  fourierdlem103  42851  fourierdlem104  42852  fourierdlem105  42853  fourierdlem106  42854  fourierdlem107  42855  fourierdlem108  42856  fourierdlem110  42858  fourierdlem111  42859  fourierdlem112  42860  fourierdlem113  42861  fourierdlem115  42863  fouriersw  42873  elaa2  42876  etransclem1  42877  etransclem5  42881  etransclem6  42882  etransclem11  42887  etransclem13  42889  etransclem41  42917  etransclem47  42923  etransc  42925  ioorrnopn  42947  ioorrnopnxr  42949  subsaliuncl  42998  sge0resplit  43045  sge0fodjrnlem  43055  nnfoctbdj  43095  iundjiun  43099  voliunsge0lem  43111  meaiuninclem  43119  meaiuninc  43120  meaiininclem  43125  meaiininc  43126  omeiunltfirp  43158  carageniuncllem2  43161  carageniuncl  43162  0ome  43168  isomennd  43170  hoicvrrex  43195  ovn0  43205  ovnsubaddlem2  43210  ovnsubadd  43211  sge0hsphoire  43228  hoidmv1lelem3  43232  hoidmv1le  43233  hoidmvlelem1  43234  hoidmvlelem2  43235  hoidmvlelem3  43236  hoidmvlelem4  43237  hoidmvlelem5  43238  hoidmvle  43239  ovnhoilem2  43241  ovnhoi  43242  hspmbllem2  43266  hspmbl  43268  hoimbl  43270  opnvonmbllem2  43272  ovnsubadd2  43285  ovolval4  43290  ovolval5lem3  43293  ovnovollem3  43297  iccvonmbl  43318  vonioolem2  43320  vonioo  43321  vonicclem2  43323  vonicc  43324  smflimlem4  43407  smfsuplem2  43443  smflimsuplem1  43451  smflimsuplem8  43458  smflimsup  43459  fundcmpsurbijinjpreimafv  43924  prproropf1o  44024  funcrngcsetcALT  44623  rmsupp0  44770  domnmsuppn0  44771  rmsuppss  44772  suppmptcfin  44781  ply1mulgsum  44798  lcoc0  44831  linc1  44834  lcoel0  44837  lcoss  44845  el0ldep  44875  lincresunit3  44890  isldepslvec2  44894  itcovalpclem2  45085  itcovalt2lem2  45090  amgmlemALT  45331