Theorem cbvmptv 5188

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 5190 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 2822	. . . 4 ⊢ (𝑥 = 𝑦 → (𝑥 ∈ 𝐴 ↔ 𝑦 ∈ 𝐴))
2		cbvmptv.1	. . . . 5 ⊢ (𝑥 = 𝑦 → 𝐵 = 𝐶)
3	2	eqeq2d 2750	. . . 4 ⊢ (𝑥 = 𝑦 → (𝑧 = 𝐵 ↔ 𝑧 = 𝐶))
4	1, 3	anbi12d 631	. . 3 ⊢ (𝑥 = 𝑦 → ((𝑥 ∈ 𝐴 ∧ 𝑧 = 𝐵) ↔ (𝑦 ∈ 𝐴 ∧ 𝑧 = 𝐶)))
5	4	cbvopab1v 5154	. 2 ⊢ {⟨𝑥, 𝑧⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑧 = 𝐵)} = {⟨𝑦, 𝑧⟩ ∣ (𝑦 ∈ 𝐴 ∧ 𝑧 = 𝐶)}
6		df-mpt 5159	. 2 ⊢ (𝑥 ∈ 𝐴 ↦ 𝐵) = {⟨𝑥, 𝑧⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑧 = 𝐵)}
7		df-mpt 5159	. 2 ⊢ (𝑦 ∈ 𝐴 ↦ 𝐶) = {⟨𝑦, 𝑧⟩ ∣ (𝑦 ∈ 𝐴 ∧ 𝑧 = 𝐶)}
8	5, 6, 7	3eqtr4i 2777	1 ⊢ (𝑥 ∈ 𝐴 ↦ 𝐵) = (𝑦 ∈ 𝐴 ↦ 𝐶)

Syntax hints:   → wi 4   ∧ wa 396   = wceq 1539   ∈ wcel 2107  {copab 5137   ↦ cmpt 5158

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 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2710

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1783  df-sb 2069  df-clab 2717  df-cleq 2731  df-clel 2817  df-rab 3074  df-v 3435  df-dif 3891  df-un 3893  df-nul 4258  df-if 4461  df-sn 4563  df-pr 4565  df-op 4569  df-opab 5138  df-mpt 5159

This theorem is referenced by:  fnmptfvd  6927  onnseq  8184  rdgsucmpt2  8270  frsucmpt2  8280  fsetfocdm  8658  fsetprcnex  8659  resixpfo  8733  pw2f1olem  8872  xpmapen  8941  dffi3  9199  ordtypecbv  9285  inf3lema  9391  cantnflem1  9456  cnfcomlem  9466  infxpenc2  9787  fseqenlem1  9789  dfac8a  9795  dfac12r  9911  r1om  10009  fictb  10010  cfsmo  10036  coftr  10038  fin23lem38  10114  compsscnv  10136  isf34lem1  10137  compss  10141  fin1a2lem1  10165  fin1a2lem3  10167  fin1a2lem13  10177  itunisuc  10184  hsmex  10197  domtriom  10208  axdc2  10214  zorn2g  10268  ttukey2g  10281  axdc  10286  konigth  10334  pwcfsdom  10348  canthp1  10419  wunex2  10503  wuncval2  10512  negiso  11964  infrenegsup  11967  rpnnen1  12732  caurcvg2  15398  caucvg  15399  summo  15438  zsum  15439  fsum  15441  ackbijnn  15549  prodmo  15655  zprod  15656  fprod  15660  iprodmul  15722  bpolyval  15768  phimullem  16489  eulerth  16493  iserodd  16545  prmreclem5  16630  prmrec  16632  vdwlem7  16697  vdwlem9  16699  vdwlem10  16700  ramub1  16738  ramcl  16739  yonedalem4c  18004  yonedalem3b  18006  gsumwspan  18494  smndex1iidm  18549  smndex1gid  18551  smndex2dlinvh  18565  grplactcnv  18687  galactghm  19021  symgfixfo  19056  pmtrdifwrdel  19102  pmtrdifwrdel2  19103  odf1o2  19187  sylow1lem2  19213  sylow1  19217  sylow2b  19237  sylow3lem1  19241  sylow3lem5  19245  sylow3  19247  efgtf  19337  efgsval  19346  ghmcyg  19506  cycsubgcyg  19511  ablfaclem3  19699  ablfac2  19701  srgbinomlem4  19788  fidomndrnglem  20587  isphld  20868  frlmphl  20997  mplmonmul  21246  evlslem2  21298  mat1ric  21645  mdetralt  21766  smadiadetlem3  21826  pmatcollpw3lem  21941  mp2pm2mplem5  21968  mp2pm2mp  21969  pm2mpmhmlem2  21977  cpmidpmat  22031  cpmadugsumlemF  22034  cpmadugsumfi  22035  cpmadumatpoly  22041  chcoeffeqlem  22043  cayleyhamilton0  22047  cayleyhamilton  22048  cayleyhamiltonALT  22049  cayleyhamilton1  22050  ordtbaslem  22348  ordtbas2  22351  lly1stc  22656  ptpjopn  22772  xkohmeo  22975  fbasrn  23044  elfm  23107  tmdmulg  23252  tmdgsum  23255  qustgpopn  23280  tsmsfbas  23288  tsmsf1o  23305  ustuqtoplem  23400  utopsnneip  23409  fmucnd  23453  ucnextcn  23465  met1stc  23686  prdsxmslem2  23694  metustto  23718  metustexhalf  23721  metuust  23725  cfilucfil2  23726  metuel  23729  metuel2  23730  psmetutop  23732  restmetu  23735  metucn  23736  xrge0tsms  24006  metdsge  24021  expcn  24044  pi1xfrcnv  24229  minveclem3b  24601  minveclem5  24606  minvec  24609  ovollb2  24662  ovolshftlem2  24683  ovolscalem2  24687  ovolicc  24696  ioombl1  24735  uniioombllem6  24761  volsup2  24778  vitali  24786  mbfi1fseq  24895  mbfmullem  24899  itg2seq  24916  itg2i1fseq  24929  itg2addlem  24932  itg2cnlem1  24935  itg2cn  24937  dvfsumrlimge0  25203  plyadd  25387  plymul  25388  coeeu  25395  coeid  25408  dvply2g  25454  plydivex  25466  elqaalem2  25489  elqaa  25491  taylthlem1  25541  taylth  25543  pserval  25578  radcnvlem2  25582  radcnvlt2  25587  dvradcnv  25589  pserulm  25590  psercn  25594  pserdvlem2  25596  pserdv  25597  efgh  25706  eff1olem  25713  circgrp  25717  circsubm  25718  logno1  25800  emcl  26161  harmonicbnd  26162  harmonicbnd2  26163  basel  26248  musum  26349  dchr1  26414  dchrptlem2  26422  dchrpt  26424  lgsqrlem4  26506  lgseisenlem3  26534  2sqlem1  26574  dchrmusumlema  26650  dchrmusum2  26651  dchrvmasumlema  26657  dchrvmasumiflem1  26658  dchrisum0ff  26664  dchrisum0lema  26671  dchrisum0lem1b  26672  dchrisum0lem2a  26674  wlknwwlksnbij  28262  clwlkclwwlken  28385  clwlknf1oclwwlkn  28457  frgrncvvdeqlem8  28679  frgrncvvdeqlem9  28680  numclwwlk1lem2  28733  ubthlem3  29243  minveco  29255  htth  29289  fsuppcurry1  31069  fsuppcurry2  31070  gsumhashmul  31325  xrge0tsmsd  31326  nsgmgc  31606  nsgqusf1olem1  31607  elrspunidl  31615  lbsdiflsp0  31716  fedgmullem1  31719  fedgmul  31721  madjusmdetlem2  31787  madjusmdet  31790  zartop  31835  zartopon  31836  zart0  31838  zarmxt1  31839  zarcmp  31841  rhmpreimacn  31844  xrge0mulc1cn  31900  xrge0tmd  31904  xrge0tmdALT  31905  gsumesum  32036  esumlub  32037  esumpcvgval  32055  esumcvg  32063  esumcvg2  32064  eulerpartlems  32336  eulerpart  32358  fibp1  32377  rrvadd  32428  ballotlemfval  32465  ballotlemi  32476  ballotlemsval  32484  ballotlemsv  32485  ballotlemsf1o  32489  ballotlemrval  32493  ballotlemrinv  32509  signsply0  32539  actfunsnf1o  32593  actfunsnrndisj  32594  itgexpif  32595  hgt750lemb  32645  derangfmla  33161  erdsze  33173  pconnpi1  33208  cvmscbv  33229  cvmsss2  33245  cvmliftlem15  33269  cvmlift2  33287  cvmlift3  33299  elmrsubrn  33491  iprodefisum  33716  nosupcbv  33914  noinfcbv  33929  knoppcnlem7  34688  knoppf  34724  f1omptsn  35517  mptsnun  35519  fin2so  35773  poimirlem27  35813  broucube  35820  ftc1anclem5  35863  ftc1anclem6  35864  sdclem2  35909  prdstotbnd  35961  prdsbnd2  35962  heiborlem10  35987  lshpkrcl  37137  tendoplcbv  38796  tendo0cbv  38807  tendoicbv  38814  lcfl7N  39522  lcf1o  39572  hdmap1cbv  39823  frlmsnic  40270  mzpclval  40554  mzpcompact2lem  40580  rmxyval  40744  dnnumch1  40876  aomclem3  40888  aomclem8  40893  dfac21  40898  pwfi2f1o  40928  dftrcl3  41335  dfrtrcl3  41348  rfovcnvf1od  41619  fsovrfovd  41624  fsovcnvlem  41628  dssmapnvod  41635  clsk3nimkb  41657  radcnvrat  41939  expgrowthi  41958  expgrowth  41960  dvradcnv2  41972  binomcxplemradcnv  41977  binomcxplemdvbinom  41978  binomcxplemdvsum  41980  binomcxplemnotnn0  41981  binomcxp  41982  wessf1ornlem  42729  projf1o  42743  fsumsermpt  43127  fmuldfeqlem1  43130  fprodcn  43148  sumnnodd  43178  limsupvaluz  43256  limsupvaluz2  43286  supcnvlimsup  43288  supcnvlimsupmpt  43289  liminfval2  43316  liminflelimsuplem  43323  fprodsubrecnncnv  43456  fprodaddrecnncnv  43458  dvsinax  43461  fperdvper  43467  dvcosax  43474  ioodvbdlimc1lem1  43479  ioodvbdlimc1  43481  ioodvbdlimc2  43483  dvnmul  43491  dvnprodlem1  43494  dvnprodlem2  43495  dvnprodlem3  43496  dvnprod  43497  itgsin0pilem1  43498  itgiccshift  43528  stoweidlem2  43550  stoweidlem17  43565  stoweidlem32  43580  stoweidlem34  43582  stoweidlem43  43591  stirlinglem2  43623  stirlinglem3  43624  stirlinglem8  43629  dirkerval  43639  dirkerval2  43642  dirkeritg  43650  dirkercncflem3  43653  dirkercncf  43655  fourierdlem14  43669  fourierdlem18  43673  fourierdlem53  43707  fourierdlem62  43716  fourierdlem71  43725  fourierdlem74  43728  fourierdlem75  43729  fourierdlem76  43730  fourierdlem80  43734  fourierdlem81  43735  fourierdlem84  43738  fourierdlem88  43742  fourierdlem92  43746  fourierdlem93  43747  fourierdlem94  43748  fourierdlem95  43749  fourierdlem96  43750  fourierdlem97  43751  fourierdlem98  43752  fourierdlem99  43753  fourierdlem101  43755  fourierdlem103  43757  fourierdlem104  43758  fourierdlem105  43759  fourierdlem106  43760  fourierdlem107  43761  fourierdlem108  43762  fourierdlem110  43764  fourierdlem111  43765  fourierdlem112  43766  fourierdlem113  43767  fourierdlem115  43769  fouriersw  43779  elaa2  43782  etransclem1  43783  etransclem5  43787  etransclem6  43788  etransclem11  43793  etransclem13  43795  etransclem41  43823  etransclem47  43829  etransc  43831  ioorrnopn  43853  ioorrnopnxr  43855  subsaliuncl  43904  sge0resplit  43951  sge0fodjrnlem  43961  nnfoctbdj  44001  iundjiun  44005  voliunsge0lem  44017  meaiuninclem  44025  meaiuninc  44026  meaiininclem  44031  meaiininc  44032  omeiunltfirp  44064  carageniuncllem2  44067  carageniuncl  44068  0ome  44074  isomennd  44076  hoicvrrex  44101  ovn0  44111  ovnsubaddlem2  44116  ovnsubadd  44117  sge0hsphoire  44134  hoidmv1lelem3  44138  hoidmv1le  44139  hoidmvlelem1  44140  hoidmvlelem2  44141  hoidmvlelem3  44142  hoidmvlelem4  44143  hoidmvlelem5  44144  hoidmvle  44145  ovnhoilem2  44147  ovnhoi  44148  hspmbllem2  44172  hspmbl  44174  hoimbl  44176  opnvonmbllem2  44178  ovnsubadd2  44191  ovolval4  44196  ovolval5lem3  44199  ovnovollem3  44203  iccvonmbl  44224  vonioolem2  44226  vonioo  44227  vonicclem2  44229  vonicc  44230  smflimlem4  44319  smfsuplem2  44356  smflimsuplem1  44364  smflimsuplem8  44371  smflimsup  44372  fundcmpsurbijinjpreimafv  44870  prproropf1o  44970  funcrngcsetcALT  45568  rmsupp0  45715  domnmsuppn0  45716  rmsuppss  45717  suppmptcfin  45726  ply1mulgsum  45742  lcoc0  45774  linc1  45777  lcoel0  45780  lcoss  45788  el0ldep  45818  lincresunit3  45833  isldepslvec2  45837  itcovalpclem2  46028  itcovalt2lem2  46033  amgmlemALT  46518