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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1912  ax-6 1971  ax-7 2016  ax-8 2114  ax-9 2122  ax-10 2143  ax-11 2159  ax-12 2176  ax-ext 2730

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 846  df-3an 1087  df-tru 1542  df-ex 1783  df-nf 1787  df-sb 2071  df-clab 2737  df-cleq 2751  df-clel 2831  df-nfc 2902  df-v 3412  df-un 3864  df-sn 4521  df-pr 4523  df-op 4527  df-opab 5093  df-mpt 5111

This theorem is referenced by:  fnmptfvd  6800  onnseq  7989  rdgsucmpt2  8074  frsucmpt2w  8083  frsucmpt2  8084  resixpfo  8516  pw2f1olem  8639  xpmapen  8704  dffi3  8918  ordtypecbv  9004  inf3lema  9110  cantnflem1  9175  cnfcomlem  9185  infxpenc2  9472  fseqenlem1  9474  dfac8a  9480  dfac12r  9596  r1om  9694  fictb  9695  cfsmo  9721  coftr  9723  fin23lem38  9799  compsscnv  9821  isf34lem1  9822  compss  9826  fin1a2lem1  9850  fin1a2lem3  9852  fin1a2lem13  9862  itunisuc  9869  hsmex  9882  domtriom  9893  axdc2  9899  zorn2g  9953  ttukey2g  9966  axdc  9971  konigth  10019  pwcfsdom  10033  canthp1  10104  wunex2  10188  wuncval2  10197  negiso  11647  infrenegsup  11650  rpnnen1  12413  caurcvg2  15072  caucvg  15073  summo  15112  zsum  15113  fsum  15115  ackbijnn  15221  prodmo  15328  zprod  15329  fprod  15333  iprodmul  15395  bpolyval  15441  phimullem  16161  eulerth  16165  iserodd  16217  prmreclem5  16301  prmrec  16303  vdwlem7  16368  vdwlem9  16370  vdwlem10  16371  ramub1  16409  ramcl  16410  yonedalem4c  17583  yonedalem3b  17585  gsumwspan  18067  smndex1iidm  18122  smndex1gid  18124  smndex2dlinvh  18138  grplactcnv  18259  galactghm  18589  symgfixfo  18624  pmtrdifwrdel  18670  pmtrdifwrdel2  18671  odf1o2  18755  sylow1lem2  18781  sylow1  18785  sylow2b  18805  sylow3lem1  18809  sylow3lem5  18813  sylow3  18815  efgtf  18905  efgsval  18914  ghmcyg  19074  cycsubgcyg  19079  ablfaclem3  19267  ablfac2  19269  srgbinomlem4  19351  fidomndrnglem  20137  isphld  20409  frlmphl  20536  mplmonmul  20786  evlslem2  20832  mat1ric  21177  mdetralt  21298  smadiadetlem3  21358  pmatcollpw3lem  21473  mp2pm2mplem5  21500  mp2pm2mp  21501  pm2mpmhmlem2  21509  cpmidpmat  21563  cpmadugsumlemF  21566  cpmadugsumfi  21567  cpmadumatpoly  21573  chcoeffeqlem  21575  cayleyhamilton0  21579  cayleyhamilton  21580  cayleyhamiltonALT  21581  cayleyhamilton1  21582  ordtbaslem  21878  ordtbas2  21881  lly1stc  22186  ptpjopn  22302  xkohmeo  22505  fbasrn  22574  elfm  22637  tmdmulg  22782  tmdgsum  22785  qustgpopn  22810  tsmsfbas  22818  tsmsf1o  22835  ustuqtoplem  22930  utopsnneip  22939  fmucnd  22983  ucnextcn  22995  met1stc  23213  prdsxmslem2  23221  metustto  23245  metustexhalf  23248  metuust  23252  cfilucfil2  23253  metuel  23256  metuel2  23257  psmetutop  23259  restmetu  23262  metucn  23263  xrge0tsms  23525  metdsge  23540  expcn  23563  pi1xfrcnv  23748  minveclem3b  24118  minveclem5  24123  minvec  24126  ovollb2  24179  ovolshftlem2  24200  ovolscalem2  24204  ovolicc  24213  ioombl1  24252  uniioombllem6  24278  volsup2  24295  vitali  24303  mbfi1fseq  24411  mbfmullem  24415  itg2seq  24432  itg2i1fseq  24445  itg2addlem  24448  itg2cnlem1  24451  itg2cn  24453  dvfsumrlimge0  24719  plyadd  24903  plymul  24904  coeeu  24911  coeid  24924  dvply2g  24970  plydivex  24982  elqaalem2  25005  elqaa  25007  taylthlem1  25057  taylth  25059  pserval  25094  radcnvlem2  25098  radcnvlt2  25103  dvradcnv  25105  pserulm  25106  psercn  25110  pserdvlem2  25112  pserdv  25113  efgh  25222  eff1olem  25229  circgrp  25233  circsubm  25234  logno1  25316  emcl  25677  harmonicbnd  25678  harmonicbnd2  25679  basel  25764  musum  25865  dchr1  25930  dchrptlem2  25938  dchrpt  25940  lgsqrlem4  26022  lgseisenlem3  26050  2sqlem1  26090  dchrmusumlema  26166  dchrmusum2  26167  dchrvmasumlema  26173  dchrvmasumiflem1  26174  dchrisum0ff  26180  dchrisum0lema  26187  dchrisum0lem1b  26188  dchrisum0lem2a  26190  wlknwwlksnbij  27763  clwlkclwwlken  27886  clwlknf1oclwwlkn  27958  frgrncvvdeqlem8  28180  frgrncvvdeqlem9  28181  numclwwlk1lem2  28234  ubthlem3  28744  minveco  28756  htth  28790  fsuppcurry1  30574  fsuppcurry2  30575  gsumhashmul  30832  xrge0tsmsd  30833  nsgmgc  31108  nsgqusf1olem1  31109  elrspunidl  31117  lbsdiflsp0  31218  fedgmullem1  31221  fedgmul  31223  madjusmdetlem2  31289  madjusmdet  31292  zartop  31337  zartopon  31338  zart0  31340  zarmxt1  31341  zarcmp  31343  rhmpreimacn  31346  xrge0mulc1cn  31402  xrge0tmd  31406  xrge0tmdALT  31407  gsumesum  31536  esumlub  31537  esumpcvgval  31555  esumcvg  31563  esumcvg2  31564  eulerpartlems  31836  eulerpart  31858  fibp1  31877  rrvadd  31928  ballotlemfval  31965  ballotlemi  31976  ballotlemsval  31984  ballotlemsv  31985  ballotlemsf1o  31989  ballotlemrval  31993  ballotlemrinv  32009  signsply0  32039  actfunsnf1o  32093  actfunsnrndisj  32094  itgexpif  32095  hgt750lemb  32145  derangfmla  32658  erdsze  32670  pconnpi1  32705  cvmscbv  32726  cvmsss2  32742  cvmliftlem15  32766  cvmlift2  32784  cvmlift3  32796  elmrsubrn  32988  iprodefisum  33212  trpredtr  33306  trpredmintr  33307  nosupcbv  33460  noinfcbv  33475  knoppcnlem7  34218  knoppf  34254  f1omptsn  35024  mptsnun  35026  fin2so  35314  poimirlem27  35354  broucube  35361  ftc1anclem5  35404  ftc1anclem6  35405  sdclem2  35450  prdstotbnd  35502  prdsbnd2  35503  heiborlem10  35528  lshpkrcl  36682  tendoplcbv  38341  tendo0cbv  38352  tendoicbv  38359  lcfl7N  39067  lcf1o  39117  hdmap1cbv  39368  frlmsnic  39760  mzpclval  40029  mzpcompact2lem  40055  rmxyval  40219  dnnumch1  40351  aomclem3  40363  aomclem8  40368  dfac21  40373  pwfi2f1o  40403  dftrcl3  40784  dfrtrcl3  40797  rfovcnvf1od  41068  fsovrfovd  41073  fsovcnvlem  41077  dssmapnvod  41084  clsk3nimkb  41106  radcnvrat  41381  expgrowthi  41400  expgrowth  41402  dvradcnv2  41414  binomcxplemradcnv  41419  binomcxplemdvbinom  41420  binomcxplemdvsum  41422  binomcxplemnotnn0  41423  binomcxp  41424  wessf1ornlem  42171  projf1o  42185  fsumsermpt  42577  fmuldfeqlem1  42580  fprodcn  42598  sumnnodd  42628  limsupvaluz  42706  limsupvaluz2  42736  supcnvlimsup  42738  supcnvlimsupmpt  42739  liminfval2  42766  liminflelimsuplem  42773  fprodsubrecnncnv  42906  fprodaddrecnncnv  42908  dvsinax  42911  fperdvper  42917  dvcosax  42924  ioodvbdlimc1lem1  42929  ioodvbdlimc1  42931  ioodvbdlimc2  42933  dvnmul  42941  dvnprodlem1  42944  dvnprodlem2  42945  dvnprodlem3  42946  dvnprod  42947  itgsin0pilem1  42948  itgiccshift  42978  stoweidlem2  43000  stoweidlem17  43015  stoweidlem32  43030  stoweidlem34  43032  stoweidlem43  43041  stirlinglem2  43073  stirlinglem3  43074  stirlinglem8  43079  dirkerval  43089  dirkerval2  43092  dirkeritg  43100  dirkercncflem3  43103  dirkercncf  43105  fourierdlem14  43119  fourierdlem18  43123  fourierdlem53  43157  fourierdlem62  43166  fourierdlem71  43175  fourierdlem74  43178  fourierdlem75  43179  fourierdlem76  43180  fourierdlem80  43184  fourierdlem81  43185  fourierdlem84  43188  fourierdlem88  43192  fourierdlem92  43196  fourierdlem93  43197  fourierdlem94  43198  fourierdlem95  43199  fourierdlem96  43200  fourierdlem97  43201  fourierdlem98  43202  fourierdlem99  43203  fourierdlem101  43205  fourierdlem103  43207  fourierdlem104  43208  fourierdlem105  43209  fourierdlem106  43210  fourierdlem107  43211  fourierdlem108  43212  fourierdlem110  43214  fourierdlem111  43215  fourierdlem112  43216  fourierdlem113  43217  fourierdlem115  43219  fouriersw  43229  elaa2  43232  etransclem1  43233  etransclem5  43237  etransclem6  43238  etransclem11  43243  etransclem13  43245  etransclem41  43273  etransclem47  43279  etransc  43281  ioorrnopn  43303  ioorrnopnxr  43305  subsaliuncl  43354  sge0resplit  43401  sge0fodjrnlem  43411  nnfoctbdj  43451  iundjiun  43455  voliunsge0lem  43467  meaiuninclem  43475  meaiuninc  43476  meaiininclem  43481  meaiininc  43482  omeiunltfirp  43514  carageniuncllem2  43517  carageniuncl  43518  0ome  43524  isomennd  43526  hoicvrrex  43551  ovn0  43561  ovnsubaddlem2  43566  ovnsubadd  43567  sge0hsphoire  43584  hoidmv1lelem3  43588  hoidmv1le  43589  hoidmvlelem1  43590  hoidmvlelem2  43591  hoidmvlelem3  43592  hoidmvlelem4  43593  hoidmvlelem5  43594  hoidmvle  43595  ovnhoilem2  43597  ovnhoi  43598  hspmbllem2  43622  hspmbl  43624  hoimbl  43626  opnvonmbllem2  43628  ovnsubadd2  43641  ovolval4  43646  ovolval5lem3  43649  ovnovollem3  43653  iccvonmbl  43674  vonioolem2  43676  vonioo  43677  vonicclem2  43679  vonicc  43680  smflimlem4  43763  smfsuplem2  43799  smflimsuplem1  43807  smflimsuplem8  43814  smflimsup  43815  fundcmpsurbijinjpreimafv  44282  prproropf1o  44382  funcrngcsetcALT  44980  rmsupp0  45127  domnmsuppn0  45128  rmsuppss  45129  suppmptcfin  45138  ply1mulgsum  45154  lcoc0  45186  linc1  45189  lcoel0  45192  lcoss  45200  el0ldep  45230  lincresunit3  45245  isldepslvec2  45249  itcovalpclem2  45440  itcovalt2lem2  45445  amgmlemALT  45686