Theorem cbvmptv 5169

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 2390. See cbvmptvg 5170 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 2977	. 2 ⊢ Ⅎ𝑦𝐵
2		nfcv 2977	. 2 ⊢ Ⅎ𝑥𝐶
3		cbvmptv.1	. 2 ⊢ (𝑥 = 𝑦 → 𝐵 = 𝐶)
4	1, 2, 3	cbvmpt 5167	1 ⊢ (𝑥 ∈ 𝐴 ↦ 𝐵) = (𝑦 ∈ 𝐴 ↦ 𝐶)

Syntax hints:   → wi 4   = wceq 1537   ↦ cmpt 5146

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2793

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3an 1085  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-rab 3147  df-v 3496  df-dif 3939  df-un 3941  df-in 3943  df-ss 3952  df-nul 4292  df-if 4468  df-sn 4568  df-pr 4570  df-op 4574  df-opab 5129  df-mpt 5147

This theorem is referenced by:  fnmptfvd  6811  onnseq  7981  rdgsucmpt2  8066  frsucmpt2w  8075  frsucmpt2  8076  resixpfo  8500  pw2f1olem  8621  xpmapen  8685  dffi3  8895  ordtypecbv  8981  inf3lema  9087  cantnflem1  9152  cnfcomlem  9162  infxpenc2  9448  fseqenlem1  9450  dfac8a  9456  dfac12r  9572  r1om  9666  fictb  9667  cfsmo  9693  coftr  9695  fin23lem38  9771  compsscnv  9793  isf34lem1  9794  compss  9798  fin1a2lem1  9822  fin1a2lem3  9824  fin1a2lem13  9834  itunisuc  9841  hsmex  9854  domtriom  9865  axdc2  9871  zorn2g  9925  ttukey2g  9938  axdc  9943  konigth  9991  pwcfsdom  10005  canthp1  10076  wunex2  10160  wuncval2  10169  negiso  11621  infrenegsup  11624  rpnnen1  12383  caurcvg2  15034  caucvg  15035  summo  15074  zsum  15075  fsum  15077  ackbijnn  15183  prodmo  15290  zprod  15291  fprod  15295  iprodmul  15357  bpolyval  15403  phimullem  16116  eulerth  16120  iserodd  16172  prmreclem5  16256  prmrec  16258  vdwlem7  16323  vdwlem9  16325  vdwlem10  16326  ramub1  16364  ramcl  16365  yonedalem4c  17527  yonedalem3b  17529  gsumwspan  18011  smndex1iidm  18066  smndex1gid  18068  smndex2dlinvh  18082  grplactcnv  18202  galactghm  18532  symgfixfo  18567  pmtrdifwrdel  18613  pmtrdifwrdel2  18614  odf1o2  18698  sylow1lem2  18724  sylow1  18728  sylow2b  18748  sylow3lem1  18752  sylow3lem5  18756  sylow3  18758  efgtf  18848  efgsval  18857  ghmcyg  19016  cycsubgcyg  19021  ablfaclem3  19209  ablfac2  19211  srgbinomlem4  19293  fidomndrnglem  20079  mplmonmul  20245  evlslem2  20292  isphld  20798  frlmphl  20925  mat1ric  21096  mdetralt  21217  smadiadetlem3  21277  pmatcollpw3lem  21391  mp2pm2mplem5  21418  mp2pm2mp  21419  pm2mpmhmlem2  21427  cpmidpmat  21481  cpmadugsumlemF  21484  cpmadugsumfi  21485  cpmadumatpoly  21491  chcoeffeqlem  21493  cayleyhamilton0  21497  cayleyhamilton  21498  cayleyhamiltonALT  21499  cayleyhamilton1  21500  ordtbaslem  21796  ordtbas2  21799  lly1stc  22104  ptpjopn  22220  xkohmeo  22423  fbasrn  22492  elfm  22555  tmdmulg  22700  tmdgsum  22703  qustgpopn  22728  tsmsfbas  22736  tsmsf1o  22753  ustuqtoplem  22848  utopsnneip  22857  fmucnd  22901  ucnextcn  22913  met1stc  23131  prdsxmslem2  23139  metustto  23163  metustexhalf  23166  metuust  23170  cfilucfil2  23171  metuel  23174  metuel2  23175  psmetutop  23177  restmetu  23180  metucn  23181  xrge0tsms  23442  metdsge  23457  expcn  23480  pi1xfrcnv  23661  minveclem3b  24031  minveclem5  24036  minvec  24039  ovollb2  24090  ovolshftlem2  24111  ovolscalem2  24115  ovolicc  24124  ioombl1  24163  uniioombllem6  24189  volsup2  24206  vitali  24214  mbfi1fseq  24322  mbfmullem  24326  itg2seq  24343  itg2i1fseq  24356  itg2addlem  24359  itg2cnlem1  24362  itg2cn  24364  dvfsumrlimge0  24627  plyadd  24807  plymul  24808  coeeu  24815  coeid  24828  dvply2g  24874  plydivex  24886  elqaalem2  24909  elqaa  24911  taylthlem1  24961  taylth  24963  pserval  24998  radcnvlem2  25002  radcnvlt2  25007  dvradcnv  25009  pserulm  25010  psercn  25014  pserdvlem2  25016  pserdv  25017  efgh  25125  eff1olem  25132  circgrp  25136  circsubm  25137  logno1  25219  emcl  25580  harmonicbnd  25581  harmonicbnd2  25582  basel  25667  musum  25768  dchr1  25833  dchrptlem2  25841  dchrpt  25843  lgsqrlem4  25925  lgseisenlem3  25953  2sqlem1  25993  dchrmusumlema  26069  dchrmusum2  26070  dchrvmasumlema  26076  dchrvmasumiflem1  26077  dchrisum0ff  26083  dchrisum0lema  26090  dchrisum0lem1b  26091  dchrisum0lem2a  26093  wlknwwlksnbij  27666  clwlkclwwlken  27790  clwlknf1oclwwlkn  27863  frgrncvvdeqlem8  28085  frgrncvvdeqlem9  28086  numclwwlk1lem2  28139  ubthlem3  28649  minveco  28661  htth  28695  fsuppcurry1  30461  fsuppcurry2  30462  xrge0tsmsd  30692  lbsdiflsp0  31022  fedgmullem1  31025  fedgmul  31027  madjusmdetlem2  31093  madjusmdet  31096  xrge0mulc1cn  31184  xrge0tmd  31188  xrge0tmdALT  31189  gsumesum  31318  esumlub  31319  esumpcvgval  31337  esumcvg  31345  esumcvg2  31346  eulerpartlems  31618  eulerpart  31640  fibp1  31659  rrvadd  31710  ballotlemfval  31747  ballotlemi  31758  ballotlemsval  31766  ballotlemsv  31767  ballotlemsf1o  31771  ballotlemrval  31775  ballotlemrinv  31791  signsply0  31821  actfunsnf1o  31875  actfunsnrndisj  31876  itgexpif  31877  hgt750lemb  31927  derangfmla  32437  erdsze  32449  pconnpi1  32484  cvmscbv  32505  cvmsss2  32521  cvmliftlem15  32545  cvmlift2  32563  cvmlift3  32575  elmrsubrn  32767  iprodefisum  32973  trpredtr  33069  trpredmintr  33070  noeta  33222  knoppcnlem7  33838  knoppf  33874  f1omptsn  34621  mptsnun  34623  fin2so  34894  poimirlem27  34934  broucube  34941  ftc1anclem5  34986  ftc1anclem6  34987  sdclem2  35032  prdstotbnd  35087  prdsbnd2  35088  heiborlem10  35113  lshpkrcl  36267  tendoplcbv  37926  tendo0cbv  37937  tendoicbv  37944  lcfl7N  38652  lcf1o  38702  hdmap1cbv  38953  frlmsnic  39198  mzpclval  39371  mzpcompact2lem  39397  rmxyval  39561  dnnumch1  39693  aomclem3  39705  aomclem8  39710  dfac21  39715  pwfi2f1o  39745  dftrcl3  40114  dfrtrcl3  40127  rfovcnvf1od  40399  fsovrfovd  40404  fsovcnvlem  40408  dssmapnvod  40415  clsk3nimkb  40439  radcnvrat  40695  expgrowthi  40714  expgrowth  40716  dvradcnv2  40728  binomcxplemradcnv  40733  binomcxplemdvbinom  40734  binomcxplemdvsum  40736  binomcxplemnotnn0  40737  binomcxp  40738  wessf1ornlem  41494  projf1o  41508  fsumsermpt  41909  fmuldfeqlem1  41912  fprodcn  41930  sumnnodd  41960  limsupvaluz  42038  limsupvaluz2  42068  supcnvlimsup  42070  supcnvlimsupmpt  42071  liminfval2  42098  liminflelimsuplem  42105  fprodsubrecnncnv  42241  fprodaddrecnncnv  42243  dvsinax  42246  fperdvper  42252  dvcosax  42260  ioodvbdlimc1lem1  42265  ioodvbdlimc1  42267  ioodvbdlimc2  42269  dvnmul  42277  dvnprodlem1  42280  dvnprodlem2  42281  dvnprodlem3  42282  dvnprod  42283  itgsin0pilem1  42284  itgiccshift  42314  stoweidlem2  42336  stoweidlem17  42351  stoweidlem32  42366  stoweidlem34  42368  stoweidlem43  42377  stirlinglem2  42409  stirlinglem3  42410  stirlinglem8  42415  dirkerval  42425  dirkerval2  42428  dirkeritg  42436  dirkercncflem3  42439  dirkercncf  42441  fourierdlem14  42455  fourierdlem18  42459  fourierdlem53  42493  fourierdlem62  42502  fourierdlem71  42511  fourierdlem74  42514  fourierdlem75  42515  fourierdlem76  42516  fourierdlem80  42520  fourierdlem81  42521  fourierdlem84  42524  fourierdlem88  42528  fourierdlem92  42532  fourierdlem93  42533  fourierdlem94  42534  fourierdlem95  42535  fourierdlem96  42536  fourierdlem97  42537  fourierdlem98  42538  fourierdlem99  42539  fourierdlem101  42541  fourierdlem103  42543  fourierdlem104  42544  fourierdlem105  42545  fourierdlem106  42546  fourierdlem107  42547  fourierdlem108  42548  fourierdlem110  42550  fourierdlem111  42551  fourierdlem112  42552  fourierdlem113  42553  fourierdlem115  42555  fouriersw  42565  elaa2  42568  etransclem1  42569  etransclem5  42573  etransclem6  42574  etransclem11  42579  etransclem13  42581  etransclem41  42609  etransclem47  42615  etransc  42617  ioorrnopn  42639  ioorrnopnxr  42641  subsaliuncl  42690  sge0resplit  42737  sge0fodjrnlem  42747  nnfoctbdj  42787  iundjiun  42791  voliunsge0lem  42803  meaiuninclem  42811  meaiuninc  42812  meaiininclem  42817  meaiininc  42818  omeiunltfirp  42850  carageniuncllem2  42853  carageniuncl  42854  0ome  42860  isomennd  42862  hoicvrrex  42887  ovn0  42897  ovnsubaddlem2  42902  ovnsubadd  42903  sge0hsphoire  42920  hoidmv1lelem3  42924  hoidmv1le  42925  hoidmvlelem1  42926  hoidmvlelem2  42927  hoidmvlelem3  42928  hoidmvlelem4  42929  hoidmvlelem5  42930  hoidmvle  42931  ovnhoilem2  42933  ovnhoi  42934  hspmbllem2  42958  hspmbl  42960  hoimbl  42962  opnvonmbllem2  42964  ovnsubadd2  42977  ovolval4  42982  ovolval5lem3  42985  ovnovollem3  42989  iccvonmbl  43010  vonioolem2  43012  vonioo  43013  vonicclem2  43015  vonicc  43016  smflimlem4  43099  smfsuplem2  43135  smflimsuplem1  43143  smflimsuplem8  43150  smflimsup  43151  fundcmpsurbijinjpreimafv  43616  prproropf1o  43718  funcrngcsetcALT  44319  rmsupp0  44465  domnmsuppn0  44466  rmsuppss  44467  suppmptcfin  44476  ply1mulgsum  44493  lcoc0  44526  linc1  44529  lcoel0  44532  lcoss  44540  el0ldep  44570  lincresunit3  44585  isldepslvec2  44589  amgmlemALT  44953