Theorem cbvmptv 5183

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 auxiliary axioms . See cbvmptvg 5185 for a less restrictive version requiring more axioms. (Revised by Gino Giotto, 17-Nov-2024.)

Hypothesis

Ref	Expression
cbvmptv.1	⊢ (𝑥 = 𝑦 → 𝐵 = 𝐶)

Assertion

Ref	Expression
cbvmptv	⊢ (𝑥 ∈ 𝐴 ↦ 𝐵) = (𝑦 ∈ 𝐴 ↦ 𝐶)

Distinct variable groups:   𝑥,𝐴,𝑦   𝑦,𝐵   𝑥,𝐶

Allowed substitution hints:   𝐵(𝑥)   𝐶(𝑦)

Proof of Theorem cbvmptv

Dummy variable 𝑧 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		eleq1w 2821	. . . 4 ⊢ (𝑥 = 𝑦 → (𝑥 ∈ 𝐴 ↔ 𝑦 ∈ 𝐴))
2		cbvmptv.1	. . . . 5 ⊢ (𝑥 = 𝑦 → 𝐵 = 𝐶)
3	2	eqeq2d 2749	. . . 4 ⊢ (𝑥 = 𝑦 → (𝑧 = 𝐵 ↔ 𝑧 = 𝐶))
4	1, 3	anbi12d 630	. . 3 ⊢ (𝑥 = 𝑦 → ((𝑥 ∈ 𝐴 ∧ 𝑧 = 𝐵) ↔ (𝑦 ∈ 𝐴 ∧ 𝑧 = 𝐶)))
5	4	cbvopab1v 5149	. 2 ⊢ {⟨𝑥, 𝑧⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑧 = 𝐵)} = {⟨𝑦, 𝑧⟩ ∣ (𝑦 ∈ 𝐴 ∧ 𝑧 = 𝐶)}
6		df-mpt 5154	. 2 ⊢ (𝑥 ∈ 𝐴 ↦ 𝐵) = {⟨𝑥, 𝑧⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑧 = 𝐵)}
7		df-mpt 5154	. 2 ⊢ (𝑦 ∈ 𝐴 ↦ 𝐶) = {⟨𝑦, 𝑧⟩ ∣ (𝑦 ∈ 𝐴 ∧ 𝑧 = 𝐶)}
8	5, 6, 7	3eqtr4i 2776	1 ⊢ (𝑥 ∈ 𝐴 ↦ 𝐵) = (𝑦 ∈ 𝐴 ↦ 𝐶)

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1539   ∈ wcel 2108  {copab 5132   ↦ cmpt 5153

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-rab 3072  df-v 3424  df-dif 3886  df-un 3888  df-nul 4254  df-if 4457  df-sn 4559  df-pr 4561  df-op 4565  df-opab 5133  df-mpt 5154

This theorem is referenced by:  fnmptfvd  6900  onnseq  8146  rdgsucmpt2  8232  frsucmpt2  8241  fsetfocdm  8607  fsetprcnex  8608  resixpfo  8682  pw2f1olem  8816  xpmapen  8881  dffi3  9120  ordtypecbv  9206  inf3lema  9312  cantnflem1  9377  cnfcomlem  9387  trpredtr  9408  trpredmintr  9409  infxpenc2  9709  fseqenlem1  9711  dfac8a  9717  dfac12r  9833  r1om  9931  fictb  9932  cfsmo  9958  coftr  9960  fin23lem38  10036  compsscnv  10058  isf34lem1  10059  compss  10063  fin1a2lem1  10087  fin1a2lem3  10089  fin1a2lem13  10099  itunisuc  10106  hsmex  10119  domtriom  10130  axdc2  10136  zorn2g  10190  ttukey2g  10203  axdc  10208  konigth  10256  pwcfsdom  10270  canthp1  10341  wunex2  10425  wuncval2  10434  negiso  11885  infrenegsup  11888  rpnnen1  12652  caurcvg2  15317  caucvg  15318  summo  15357  zsum  15358  fsum  15360  ackbijnn  15468  prodmo  15574  zprod  15575  fprod  15579  iprodmul  15641  bpolyval  15687  phimullem  16408  eulerth  16412  iserodd  16464  prmreclem5  16549  prmrec  16551  vdwlem7  16616  vdwlem9  16618  vdwlem10  16619  ramub1  16657  ramcl  16658  yonedalem4c  17911  yonedalem3b  17913  gsumwspan  18400  smndex1iidm  18455  smndex1gid  18457  smndex2dlinvh  18471  grplactcnv  18593  galactghm  18927  symgfixfo  18962  pmtrdifwrdel  19008  pmtrdifwrdel2  19009  odf1o2  19093  sylow1lem2  19119  sylow1  19123  sylow2b  19143  sylow3lem1  19147  sylow3lem5  19151  sylow3  19153  efgtf  19243  efgsval  19252  ghmcyg  19412  cycsubgcyg  19417  ablfaclem3  19605  ablfac2  19607  srgbinomlem4  19694  fidomndrnglem  20491  isphld  20771  frlmphl  20898  mplmonmul  21147  evlslem2  21199  mat1ric  21544  mdetralt  21665  smadiadetlem3  21725  pmatcollpw3lem  21840  mp2pm2mplem5  21867  mp2pm2mp  21868  pm2mpmhmlem2  21876  cpmidpmat  21930  cpmadugsumlemF  21933  cpmadugsumfi  21934  cpmadumatpoly  21940  chcoeffeqlem  21942  cayleyhamilton0  21946  cayleyhamilton  21947  cayleyhamiltonALT  21948  cayleyhamilton1  21949  ordtbaslem  22247  ordtbas2  22250  lly1stc  22555  ptpjopn  22671  xkohmeo  22874  fbasrn  22943  elfm  23006  tmdmulg  23151  tmdgsum  23154  qustgpopn  23179  tsmsfbas  23187  tsmsf1o  23204  ustuqtoplem  23299  utopsnneip  23308  fmucnd  23352  ucnextcn  23364  met1stc  23583  prdsxmslem2  23591  metustto  23615  metustexhalf  23618  metuust  23622  cfilucfil2  23623  metuel  23626  metuel2  23627  psmetutop  23629  restmetu  23632  metucn  23633  xrge0tsms  23903  metdsge  23918  expcn  23941  pi1xfrcnv  24126  minveclem3b  24497  minveclem5  24502  minvec  24505  ovollb2  24558  ovolshftlem2  24579  ovolscalem2  24583  ovolicc  24592  ioombl1  24631  uniioombllem6  24657  volsup2  24674  vitali  24682  mbfi1fseq  24791  mbfmullem  24795  itg2seq  24812  itg2i1fseq  24825  itg2addlem  24828  itg2cnlem1  24831  itg2cn  24833  dvfsumrlimge0  25099  plyadd  25283  plymul  25284  coeeu  25291  coeid  25304  dvply2g  25350  plydivex  25362  elqaalem2  25385  elqaa  25387  taylthlem1  25437  taylth  25439  pserval  25474  radcnvlem2  25478  radcnvlt2  25483  dvradcnv  25485  pserulm  25486  psercn  25490  pserdvlem2  25492  pserdv  25493  efgh  25602  eff1olem  25609  circgrp  25613  circsubm  25614  logno1  25696  emcl  26057  harmonicbnd  26058  harmonicbnd2  26059  basel  26144  musum  26245  dchr1  26310  dchrptlem2  26318  dchrpt  26320  lgsqrlem4  26402  lgseisenlem3  26430  2sqlem1  26470  dchrmusumlema  26546  dchrmusum2  26547  dchrvmasumlema  26553  dchrvmasumiflem1  26554  dchrisum0ff  26560  dchrisum0lema  26567  dchrisum0lem1b  26568  dchrisum0lem2a  26570  wlknwwlksnbij  28154  clwlkclwwlken  28277  clwlknf1oclwwlkn  28349  frgrncvvdeqlem8  28571  frgrncvvdeqlem9  28572  numclwwlk1lem2  28625  ubthlem3  29135  minveco  29147  htth  29181  fsuppcurry1  30962  fsuppcurry2  30963  gsumhashmul  31218  xrge0tsmsd  31219  nsgmgc  31499  nsgqusf1olem1  31500  elrspunidl  31508  lbsdiflsp0  31609  fedgmullem1  31612  fedgmul  31614  madjusmdetlem2  31680  madjusmdet  31683  zartop  31728  zartopon  31729  zart0  31731  zarmxt1  31732  zarcmp  31734  rhmpreimacn  31737  xrge0mulc1cn  31793  xrge0tmd  31797  xrge0tmdALT  31798  gsumesum  31927  esumlub  31928  esumpcvgval  31946  esumcvg  31954  esumcvg2  31955  eulerpartlems  32227  eulerpart  32249  fibp1  32268  rrvadd  32319  ballotlemfval  32356  ballotlemi  32367  ballotlemsval  32375  ballotlemsv  32376  ballotlemsf1o  32380  ballotlemrval  32384  ballotlemrinv  32400  signsply0  32430  actfunsnf1o  32484  actfunsnrndisj  32485  itgexpif  32486  hgt750lemb  32536  derangfmla  33052  erdsze  33064  pconnpi1  33099  cvmscbv  33120  cvmsss2  33136  cvmliftlem15  33160  cvmlift2  33178  cvmlift3  33190  elmrsubrn  33382  iprodefisum  33613  nosupcbv  33832  noinfcbv  33847  knoppcnlem7  34606  knoppf  34642  f1omptsn  35435  mptsnun  35437  fin2so  35691  poimirlem27  35731  broucube  35738  ftc1anclem5  35781  ftc1anclem6  35782  sdclem2  35827  prdstotbnd  35879  prdsbnd2  35880  heiborlem10  35905  lshpkrcl  37057  tendoplcbv  38716  tendo0cbv  38727  tendoicbv  38734  lcfl7N  39442  lcf1o  39492  hdmap1cbv  39743  frlmsnic  40188  mzpclval  40463  mzpcompact2lem  40489  rmxyval  40653  dnnumch1  40785  aomclem3  40797  aomclem8  40802  dfac21  40807  pwfi2f1o  40837  dftrcl3  41217  dfrtrcl3  41230  rfovcnvf1od  41501  fsovrfovd  41506  fsovcnvlem  41510  dssmapnvod  41517  clsk3nimkb  41539  radcnvrat  41821  expgrowthi  41840  expgrowth  41842  dvradcnv2  41854  binomcxplemradcnv  41859  binomcxplemdvbinom  41860  binomcxplemdvsum  41862  binomcxplemnotnn0  41863  binomcxp  41864  wessf1ornlem  42611  projf1o  42625  fsumsermpt  43010  fmuldfeqlem1  43013  fprodcn  43031  sumnnodd  43061  limsupvaluz  43139  limsupvaluz2  43169  supcnvlimsup  43171  supcnvlimsupmpt  43172  liminfval2  43199  liminflelimsuplem  43206  fprodsubrecnncnv  43339  fprodaddrecnncnv  43341  dvsinax  43344  fperdvper  43350  dvcosax  43357  ioodvbdlimc1lem1  43362  ioodvbdlimc1  43364  ioodvbdlimc2  43366  dvnmul  43374  dvnprodlem1  43377  dvnprodlem2  43378  dvnprodlem3  43379  dvnprod  43380  itgsin0pilem1  43381  itgiccshift  43411  stoweidlem2  43433  stoweidlem17  43448  stoweidlem32  43463  stoweidlem34  43465  stoweidlem43  43474  stirlinglem2  43506  stirlinglem3  43507  stirlinglem8  43512  dirkerval  43522  dirkerval2  43525  dirkeritg  43533  dirkercncflem3  43536  dirkercncf  43538  fourierdlem14  43552  fourierdlem18  43556  fourierdlem53  43590  fourierdlem62  43599  fourierdlem71  43608  fourierdlem74  43611  fourierdlem75  43612  fourierdlem76  43613  fourierdlem80  43617  fourierdlem81  43618  fourierdlem84  43621  fourierdlem88  43625  fourierdlem92  43629  fourierdlem93  43630  fourierdlem94  43631  fourierdlem95  43632  fourierdlem96  43633  fourierdlem97  43634  fourierdlem98  43635  fourierdlem99  43636  fourierdlem101  43638  fourierdlem103  43640  fourierdlem104  43641  fourierdlem105  43642  fourierdlem106  43643  fourierdlem107  43644  fourierdlem108  43645  fourierdlem110  43647  fourierdlem111  43648  fourierdlem112  43649  fourierdlem113  43650  fourierdlem115  43652  fouriersw  43662  elaa2  43665  etransclem1  43666  etransclem5  43670  etransclem6  43671  etransclem11  43676  etransclem13  43678  etransclem41  43706  etransclem47  43712  etransc  43714  ioorrnopn  43736  ioorrnopnxr  43738  subsaliuncl  43787  sge0resplit  43834  sge0fodjrnlem  43844  nnfoctbdj  43884  iundjiun  43888  voliunsge0lem  43900  meaiuninclem  43908  meaiuninc  43909  meaiininclem  43914  meaiininc  43915  omeiunltfirp  43947  carageniuncllem2  43950  carageniuncl  43951  0ome  43957  isomennd  43959  hoicvrrex  43984  ovn0  43994  ovnsubaddlem2  43999  ovnsubadd  44000  sge0hsphoire  44017  hoidmv1lelem3  44021  hoidmv1le  44022  hoidmvlelem1  44023  hoidmvlelem2  44024  hoidmvlelem3  44025  hoidmvlelem4  44026  hoidmvlelem5  44027  hoidmvle  44028  ovnhoilem2  44030  ovnhoi  44031  hspmbllem2  44055  hspmbl  44057  hoimbl  44059  opnvonmbllem2  44061  ovnsubadd2  44074  ovolval4  44079  ovolval5lem3  44082  ovnovollem3  44086  iccvonmbl  44107  vonioolem2  44109  vonioo  44110  vonicclem2  44112  vonicc  44113  smflimlem4  44196  smfsuplem2  44232  smflimsuplem1  44240  smflimsuplem8  44247  smflimsup  44248  fundcmpsurbijinjpreimafv  44747  prproropf1o  44847  funcrngcsetcALT  45445  rmsupp0  45592  domnmsuppn0  45593  rmsuppss  45594  suppmptcfin  45603  ply1mulgsum  45619  lcoc0  45651  linc1  45654  lcoel0  45657  lcoss  45665  el0ldep  45695  lincresunit3  45710  isldepslvec2  45714  itcovalpclem2  45905  itcovalt2lem2  45910  amgmlemALT  46393