Theorem cbvmptv 5255

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 5257 for a less restrictive version requiring more axioms. (Revised by GG, 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 2824	. . . 4 ⊢ (𝑥 = 𝑦 → (𝑥 ∈ 𝐴 ↔ 𝑦 ∈ 𝐴))
2		cbvmptv.1	. . . . 5 ⊢ (𝑥 = 𝑦 → 𝐵 = 𝐶)
3	2	eqeq2d 2748	. . . 4 ⊢ (𝑥 = 𝑦 → (𝑧 = 𝐵 ↔ 𝑧 = 𝐶))
4	1, 3	anbi12d 632	. . 3 ⊢ (𝑥 = 𝑦 → ((𝑥 ∈ 𝐴 ∧ 𝑧 = 𝐵) ↔ (𝑦 ∈ 𝐴 ∧ 𝑧 = 𝐶)))
5	4	cbvopab1v 5221	. 2 ⊢ {⟨𝑥, 𝑧⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑧 = 𝐵)} = {⟨𝑦, 𝑧⟩ ∣ (𝑦 ∈ 𝐴 ∧ 𝑧 = 𝐶)}
6		df-mpt 5226	. 2 ⊢ (𝑥 ∈ 𝐴 ↦ 𝐵) = {⟨𝑥, 𝑧⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑧 = 𝐵)}
7		df-mpt 5226	. 2 ⊢ (𝑦 ∈ 𝐴 ↦ 𝐶) = {⟨𝑦, 𝑧⟩ ∣ (𝑦 ∈ 𝐴 ∧ 𝑧 = 𝐶)}
8	5, 6, 7	3eqtr4i 2775	1 ⊢ (𝑥 ∈ 𝐴 ↦ 𝐵) = (𝑦 ∈ 𝐴 ↦ 𝐶)

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1540   ∈ wcel 2108  {copab 5205   ↦ cmpt 5225

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-rab 3437  df-v 3482  df-dif 3954  df-un 3956  df-ss 3968  df-nul 4334  df-if 4526  df-sn 4627  df-pr 4629  df-op 4633  df-opab 5206  df-mpt 5226

This theorem is referenced by:  fnmptfvd  7061  mptcnfimad  8011  onnseq  8384  rdgsucmpt2  8470  frsucmpt2  8480  fsetfocdm  8901  fsetprcnex  8902  resixpfo  8976  pw2f1olem  9116  xpmapen  9185  dffi3  9471  ordtypecbv  9557  inf3lema  9664  cantnflem1  9729  cnfcomlem  9739  infxpenc2  10062  fseqenlem1  10064  dfac8a  10070  dfac12r  10187  r1om  10283  fictb  10284  cfsmo  10311  coftr  10313  fin23lem38  10389  compsscnv  10411  isf34lem1  10412  compss  10416  fin1a2lem1  10440  fin1a2lem3  10442  fin1a2lem13  10452  itunisuc  10459  hsmex  10472  domtriom  10483  axdc2  10489  zorn2g  10543  ttukey2g  10556  axdc  10561  konigth  10609  pwcfsdom  10623  canthp1  10694  wunex2  10778  wuncval2  10787  negiso  12248  infrenegsup  12251  rpnnen1  13025  caurcvg2  15714  caucvg  15715  summo  15753  zsum  15754  fsum  15756  ackbijnn  15864  cbvprodv  15950  prodmo  15972  zprod  15973  fprod  15977  iprodmul  16039  bpolyval  16085  phimullem  16816  eulerth  16820  iserodd  16873  prmreclem5  16958  prmrec  16960  vdwlem7  17025  vdwlem9  17027  vdwlem10  17028  ramub1  17066  ramcl  17067  yonedalem4c  18322  yonedalem3b  18324  gsumwspan  18859  smndex1iidm  18914  smndex1gid  18916  smndex2dlinvh  18930  grplactcnv  19061  gicqusker  19306  galactghm  19422  symgfixfo  19457  pmtrdifwrdel  19503  pmtrdifwrdel2  19504  odf1o2  19591  sylow1lem2  19617  sylow1  19621  sylow2b  19641  sylow3lem1  19645  sylow3lem5  19649  sylow3  19651  efgtf  19740  efgsval  19749  ghmcyg  19914  cycsubgcyg  19919  ablfaclem3  20107  ablfac2  20109  srgbinomlem4  20226  funcrngcsetcALT  20641  fidomndrnglem  20773  isphld  21672  frlmphl  21801  mplmonmul  22054  evlslem2  22103  mat1ric  22493  mdetralt  22614  smadiadetlem3  22674  pmatcollpw3lem  22789  mp2pm2mplem5  22816  mp2pm2mp  22817  pm2mpmhmlem2  22825  cpmidpmat  22879  cpmadugsumlemF  22882  cpmadugsumfi  22883  cpmadumatpoly  22889  chcoeffeqlem  22891  cayleyhamilton0  22895  cayleyhamilton  22896  cayleyhamiltonALT  22897  cayleyhamilton1  22898  ordtbaslem  23196  ordtbas2  23199  lly1stc  23504  ptpjopn  23620  xkohmeo  23823  fbasrn  23892  elfm  23955  tmdmulg  24100  tmdgsum  24103  qustgpopn  24128  tsmsfbas  24136  tsmsf1o  24153  ustuqtoplem  24248  utopsnneip  24257  fmucnd  24301  ucnextcn  24313  met1stc  24534  prdsxmslem2  24542  metustto  24566  metustexhalf  24569  metuust  24573  cfilucfil2  24574  metuel  24577  metuel2  24578  psmetutop  24580  restmetu  24583  metucn  24584  xrge0tsms  24856  metdsge  24871  expcn  24896  expcnOLD  24898  pi1xfrcnv  25090  minveclem3b  25462  minveclem5  25467  minvec  25470  ovollb2  25524  ovolshftlem2  25545  ovolscalem2  25549  ovolicc  25558  ioombl1  25597  uniioombllem6  25623  volsup2  25640  vitali  25648  mbfi1fseq  25756  mbfmullem  25760  itg2seq  25777  itg2i1fseq  25790  itg2addlem  25793  itg2cnlem1  25796  itg2cn  25798  cbvitgv  25812  dvfsumrlimge0  26071  plyadd  26256  plymul  26257  coeeu  26264  coeid  26277  dvply2g  26326  dvply2gOLD  26327  plydivex  26339  elqaalem2  26362  elqaa  26364  taylthlem1  26415  taylth  26418  pserval  26453  radcnvlem2  26457  radcnvlt2  26462  dvradcnv  26464  pserulm  26465  psercn  26470  pserdvlem2  26472  pserdv  26473  efgh  26583  eff1olem  26590  circgrp  26594  circsubm  26595  logno1  26678  emcl  27046  harmonicbnd  27047  harmonicbnd2  27048  basel  27133  musum  27234  dchr1  27301  dchrptlem2  27309  dchrpt  27311  lgsqrlem4  27393  lgseisenlem3  27421  2sqlem1  27461  dchrmusumlema  27537  dchrmusum2  27538  dchrvmasumlema  27544  dchrvmasumiflem1  27545  dchrisum0ff  27551  dchrisum0lema  27558  dchrisum0lem1b  27559  dchrisum0lem2a  27561  nosupcbv  27747  noinfcbv  27762  precsexlemcbv  28230  seqsfn  28315  seqsp1  28317  wlknwwlksnbij  29908  clwlkclwwlken  30031  clwlknf1oclwwlkn  30103  frgrncvvdeqlem8  30325  frgrncvvdeqlem9  30326  numclwwlk1lem2  30379  ubthlem3  30891  minveco  30903  htth  30937  fsuppcurry1  32736  fsuppcurry2  32737  gsumhashmul  33064  xrge0tsmsd  33065  elrgspnlem1  33246  elrgspnlem2  33247  elrgspn  33250  elrgspnsubrunlem1  33251  elrgspnsubrunlem2  33252  elrgspnsubrun  33253  idomsubr  33311  nsgmgc  33440  nsgqusf1olem1  33441  lmicqusker  33446  ricqusker  33455  elrspunidl  33456  elrspunsn  33457  zringfrac  33582  ply1degltdim  33674  lbsdiflsp0  33677  fedgmullem1  33680  fedgmul  33682  assarrginv  33687  evls1fldgencl  33720  fldextrspunlsplem  33723  fldextrspunlsp  33724  algextdeglem4  33761  algextdeg  33766  madjusmdetlem2  33827  madjusmdet  33830  zartop  33875  zartopon  33876  zart0  33878  zarmxt1  33879  zarcmp  33881  rhmpreimacn  33884  xrge0mulc1cn  33940  xrge0tmd  33944  xrge0tmdALT  33945  cbvesumv  34044  gsumesum  34060  esumlub  34061  esumpcvgval  34079  esumcvg  34087  esumcvg2  34088  eulerpartlems  34362  eulerpart  34384  fibp1  34403  rrvadd  34454  ballotlemfval  34492  ballotlemi  34503  ballotlemsval  34511  ballotlemsv  34512  ballotlemsf1o  34516  ballotlemrval  34520  ballotlemrinv  34536  signsply0  34566  actfunsnf1o  34619  actfunsnrndisj  34620  itgexpif  34621  hgt750lemb  34671  derangfmla  35195  erdsze  35207  pconnpi1  35242  cvmscbv  35263  cvmsss2  35279  cvmliftlem15  35303  cvmlift2  35321  cvmlift3  35333  elmrsubrn  35525  iprodefisum  35741  cbvprodvw2  36248  cbvitgvw2  36249  knoppcnlem7  36500  knoppf  36536  f1omptsn  37338  mptsnun  37340  fin2so  37614  poimirlem27  37654  broucube  37661  ftc1anclem5  37704  ftc1anclem6  37705  sdclem2  37749  prdstotbnd  37801  prdsbnd2  37802  heiborlem10  37827  lshpkrcl  39117  tendoplcbv  40777  tendo0cbv  40788  tendoicbv  40795  lcfl7N  41503  lcf1o  41553  hdmap1cbv  41804  frlmsnic  42550  evlselv  42597  mzpclval  42736  mzpcompact2lem  42762  rmxyval  42927  dnnumch1  43056  aomclem3  43068  aomclem8  43073  dfac21  43078  pwfi2f1o  43108  dftrcl3  43733  dfrtrcl3  43746  rfovcnvf1od  44017  fsovrfovd  44022  fsovcnvlem  44026  dssmapnvod  44033  clsk3nimkb  44053  radcnvrat  44333  expgrowthi  44352  expgrowth  44354  dvradcnv2  44366  binomcxplemradcnv  44371  binomcxplemdvbinom  44372  binomcxplemdvsum  44374  binomcxplemnotnn0  44375  binomcxp  44376  wessf1ornlem  45190  projf1o  45202  fsumsermpt  45594  fmuldfeqlem1  45597  fprodcn  45615  sumnnodd  45645  limsupvaluz  45723  limsupvaluz2  45753  supcnvlimsup  45755  supcnvlimsupmpt  45756  liminfval2  45783  liminflelimsuplem  45790  fprodsubrecnncnv  45923  fprodaddrecnncnv  45925  dvsinax  45928  fperdvper  45934  dvcosax  45941  ioodvbdlimc1lem1  45946  ioodvbdlimc1  45948  ioodvbdlimc2  45950  dvnmul  45958  dvnprodlem1  45961  dvnprodlem2  45962  dvnprodlem3  45963  dvnprod  45964  itgsin0pilem1  45965  itgiccshift  45995  stoweidlem2  46017  stoweidlem17  46032  stoweidlem32  46047  stoweidlem34  46049  stoweidlem43  46058  stirlinglem2  46090  stirlinglem3  46091  stirlinglem8  46096  dirkerval  46106  dirkerval2  46109  dirkeritg  46117  dirkercncflem3  46120  dirkercncf  46122  fourierdlem14  46136  fourierdlem18  46140  fourierdlem53  46174  fourierdlem62  46183  fourierdlem71  46192  fourierdlem74  46195  fourierdlem75  46196  fourierdlem76  46197  fourierdlem80  46201  fourierdlem81  46202  fourierdlem84  46205  fourierdlem88  46209  fourierdlem92  46213  fourierdlem93  46214  fourierdlem94  46215  fourierdlem95  46216  fourierdlem96  46217  fourierdlem97  46218  fourierdlem98  46219  fourierdlem99  46220  fourierdlem101  46222  fourierdlem103  46224  fourierdlem104  46225  fourierdlem105  46226  fourierdlem106  46227  fourierdlem107  46228  fourierdlem108  46229  fourierdlem110  46231  fourierdlem111  46232  fourierdlem112  46233  fourierdlem113  46234  fourierdlem115  46236  fouriersw  46246  elaa2  46249  etransclem1  46250  etransclem5  46254  etransclem6  46255  etransclem11  46260  etransclem13  46262  etransclem41  46290  etransclem47  46296  etransc  46298  ioorrnopn  46320  ioorrnopnxr  46322  subsaliuncl  46373  sge0resplit  46421  sge0fodjrnlem  46431  nnfoctbdj  46471  iundjiun  46475  voliunsge0lem  46487  meaiuninclem  46495  meaiuninc  46496  meaiininclem  46501  meaiininc  46502  omeiunltfirp  46534  carageniuncllem2  46537  carageniuncl  46538  0ome  46544  isomennd  46546  hoicvrrex  46571  ovn0  46581  ovnsubaddlem2  46586  ovnsubadd  46587  sge0hsphoire  46604  hoidmv1lelem3  46608  hoidmv1le  46609  hoidmvlelem1  46610  hoidmvlelem2  46611  hoidmvlelem3  46612  hoidmvlelem4  46613  hoidmvlelem5  46614  hoidmvle  46615  ovnhoilem2  46617  ovnhoi  46618  hspmbllem2  46642  hspmbl  46644  hoimbl  46646  opnvonmbllem2  46648  ovnsubadd2  46661  ovolval4  46666  ovolval5lem3  46669  ovnovollem3  46673  iccvonmbl  46694  vonioolem2  46696  vonioo  46697  vonicclem2  46699  vonicc  46700  smflimlem4  46789  smfsuplem2  46827  smflimsuplem1  46835  smflimsuplem8  46842  smflimsup  46843  fundcmpsurbijinjpreimafv  47394  prproropf1o  47494  isuspgrim0  47872  uspgrimprop  47873  isubgr3stgrlem8  47940  rmsupp0  48284  domnmsuppn0  48285  rmsuppss  48286  suppmptcfin  48292  ply1mulgsum  48307  lcoc0  48339  linc1  48342  lcoel0  48345  lcoss  48353  el0ldep  48383  lincresunit3  48398  isldepslvec2  48402  itcovalpclem2  48592  itcovalt2lem2  48597  amgmlemALT  49322