Theorem cbvmptv 5279

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 5281 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 2827	. . . 4 ⊢ (𝑥 = 𝑦 → (𝑥 ∈ 𝐴 ↔ 𝑦 ∈ 𝐴))
2		cbvmptv.1	. . . . 5 ⊢ (𝑥 = 𝑦 → 𝐵 = 𝐶)
3	2	eqeq2d 2751	. . . 4 ⊢ (𝑥 = 𝑦 → (𝑧 = 𝐵 ↔ 𝑧 = 𝐶))
4	1, 3	anbi12d 631	. . 3 ⊢ (𝑥 = 𝑦 → ((𝑥 ∈ 𝐴 ∧ 𝑧 = 𝐵) ↔ (𝑦 ∈ 𝐴 ∧ 𝑧 = 𝐶)))
5	4	cbvopab1v 5245	. 2 ⊢ {⟨𝑥, 𝑧⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑧 = 𝐵)} = {⟨𝑦, 𝑧⟩ ∣ (𝑦 ∈ 𝐴 ∧ 𝑧 = 𝐶)}
6		df-mpt 5250	. 2 ⊢ (𝑥 ∈ 𝐴 ↦ 𝐵) = {⟨𝑥, 𝑧⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑧 = 𝐵)}
7		df-mpt 5250	. 2 ⊢ (𝑦 ∈ 𝐴 ↦ 𝐶) = {⟨𝑦, 𝑧⟩ ∣ (𝑦 ∈ 𝐴 ∧ 𝑧 = 𝐶)}
8	5, 6, 7	3eqtr4i 2778	1 ⊢ (𝑥 ∈ 𝐴 ↦ 𝐵) = (𝑦 ∈ 𝐴 ↦ 𝐶)

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1537   ∈ wcel 2108  {copab 5228   ↦ cmpt 5249

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 847  df-3an 1089  df-tru 1540  df-fal 1550  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-rab 3444  df-v 3490  df-dif 3979  df-un 3981  df-ss 3993  df-nul 4353  df-if 4549  df-sn 4649  df-pr 4651  df-op 4655  df-opab 5229  df-mpt 5250

This theorem is referenced by:  fnmptfvd  7074  mptcnfimad  8027  onnseq  8400  rdgsucmpt2  8486  frsucmpt2  8496  fsetfocdm  8919  fsetprcnex  8920  resixpfo  8994  pw2f1olem  9142  xpmapen  9211  dffi3  9500  ordtypecbv  9586  inf3lema  9693  cantnflem1  9758  cnfcomlem  9768  infxpenc2  10091  fseqenlem1  10093  dfac8a  10099  dfac12r  10216  r1om  10312  fictb  10313  cfsmo  10340  coftr  10342  fin23lem38  10418  compsscnv  10440  isf34lem1  10441  compss  10445  fin1a2lem1  10469  fin1a2lem3  10471  fin1a2lem13  10481  itunisuc  10488  hsmex  10501  domtriom  10512  axdc2  10518  zorn2g  10572  ttukey2g  10585  axdc  10590  konigth  10638  pwcfsdom  10652  canthp1  10723  wunex2  10807  wuncval2  10816  negiso  12275  infrenegsup  12278  rpnnen1  13048  caurcvg2  15726  caucvg  15727  summo  15765  zsum  15766  fsum  15768  ackbijnn  15876  cbvprodv  15962  prodmo  15984  zprod  15985  fprod  15989  iprodmul  16051  bpolyval  16097  phimullem  16826  eulerth  16830  iserodd  16882  prmreclem5  16967  prmrec  16969  vdwlem7  17034  vdwlem9  17036  vdwlem10  17037  ramub1  17075  ramcl  17076  yonedalem4c  18347  yonedalem3b  18349  gsumwspan  18881  smndex1iidm  18936  smndex1gid  18938  smndex2dlinvh  18952  grplactcnv  19083  gicqusker  19328  galactghm  19446  symgfixfo  19481  pmtrdifwrdel  19527  pmtrdifwrdel2  19528  odf1o2  19615  sylow1lem2  19641  sylow1  19645  sylow2b  19665  sylow3lem1  19669  sylow3lem5  19673  sylow3  19675  efgtf  19764  efgsval  19773  ghmcyg  19938  cycsubgcyg  19943  ablfaclem3  20131  ablfac2  20133  srgbinomlem4  20256  funcrngcsetcALT  20663  fidomndrnglem  20795  isphld  21695  frlmphl  21824  mplmonmul  22077  evlslem2  22126  mat1ric  22514  mdetralt  22635  smadiadetlem3  22695  pmatcollpw3lem  22810  mp2pm2mplem5  22837  mp2pm2mp  22838  pm2mpmhmlem2  22846  cpmidpmat  22900  cpmadugsumlemF  22903  cpmadugsumfi  22904  cpmadumatpoly  22910  chcoeffeqlem  22912  cayleyhamilton0  22916  cayleyhamilton  22917  cayleyhamiltonALT  22918  cayleyhamilton1  22919  ordtbaslem  23217  ordtbas2  23220  lly1stc  23525  ptpjopn  23641  xkohmeo  23844  fbasrn  23913  elfm  23976  tmdmulg  24121  tmdgsum  24124  qustgpopn  24149  tsmsfbas  24157  tsmsf1o  24174  ustuqtoplem  24269  utopsnneip  24278  fmucnd  24322  ucnextcn  24334  met1stc  24555  prdsxmslem2  24563  metustto  24587  metustexhalf  24590  metuust  24594  cfilucfil2  24595  metuel  24598  metuel2  24599  psmetutop  24601  restmetu  24604  metucn  24605  xrge0tsms  24875  metdsge  24890  expcn  24915  expcnOLD  24917  pi1xfrcnv  25109  minveclem3b  25481  minveclem5  25486  minvec  25489  ovollb2  25543  ovolshftlem2  25564  ovolscalem2  25568  ovolicc  25577  ioombl1  25616  uniioombllem6  25642  volsup2  25659  vitali  25667  mbfi1fseq  25776  mbfmullem  25780  itg2seq  25797  itg2i1fseq  25810  itg2addlem  25813  itg2cnlem1  25816  itg2cn  25818  cbvitgv  25832  dvfsumrlimge0  26091  plyadd  26276  plymul  26277  coeeu  26284  coeid  26297  dvply2g  26344  dvply2gOLD  26345  plydivex  26357  elqaalem2  26380  elqaa  26382  taylthlem1  26433  taylth  26436  pserval  26471  radcnvlem2  26475  radcnvlt2  26480  dvradcnv  26482  pserulm  26483  psercn  26488  pserdvlem2  26490  pserdv  26491  efgh  26601  eff1olem  26608  circgrp  26612  circsubm  26613  logno1  26696  emcl  27064  harmonicbnd  27065  harmonicbnd2  27066  basel  27151  musum  27252  dchr1  27319  dchrptlem2  27327  dchrpt  27329  lgsqrlem4  27411  lgseisenlem3  27439  2sqlem1  27479  dchrmusumlema  27555  dchrmusum2  27556  dchrvmasumlema  27562  dchrvmasumiflem1  27563  dchrisum0ff  27569  dchrisum0lema  27576  dchrisum0lem1b  27577  dchrisum0lem2a  27579  nosupcbv  27765  noinfcbv  27780  precsexlemcbv  28248  seqsfn  28333  seqsp1  28335  wlknwwlksnbij  29921  clwlkclwwlken  30044  clwlknf1oclwwlkn  30116  frgrncvvdeqlem8  30338  frgrncvvdeqlem9  30339  numclwwlk1lem2  30392  ubthlem3  30904  minveco  30916  htth  30950  fsuppcurry1  32739  fsuppcurry2  32740  gsumhashmul  33040  xrge0tsmsd  33041  idomsubr  33276  nsgmgc  33405  nsgqusf1olem1  33406  lmicqusker  33411  ricqusker  33420  elrspunidl  33421  elrspunsn  33422  zringfrac  33547  ply1degltdim  33636  lbsdiflsp0  33639  fedgmullem1  33642  fedgmul  33644  assarrginv  33649  evls1fldgencl  33680  algextdeglem4  33711  algextdeg  33716  madjusmdetlem2  33774  madjusmdet  33777  zartop  33822  zartopon  33823  zart0  33825  zarmxt1  33826  zarcmp  33828  rhmpreimacn  33831  xrge0mulc1cn  33887  xrge0tmd  33891  xrge0tmdALT  33892  cbvesumv  34007  gsumesum  34023  esumlub  34024  esumpcvgval  34042  esumcvg  34050  esumcvg2  34051  eulerpartlems  34325  eulerpart  34347  fibp1  34366  rrvadd  34417  ballotlemfval  34454  ballotlemi  34465  ballotlemsval  34473  ballotlemsv  34474  ballotlemsf1o  34478  ballotlemrval  34482  ballotlemrinv  34498  signsply0  34528  actfunsnf1o  34581  actfunsnrndisj  34582  itgexpif  34583  hgt750lemb  34633  derangfmla  35158  erdsze  35170  pconnpi1  35205  cvmscbv  35226  cvmsss2  35242  cvmliftlem15  35266  cvmlift2  35284  cvmlift3  35296  elmrsubrn  35488  iprodefisum  35703  cbvprodvw2  36213  cbvitgvw2  36214  knoppcnlem7  36465  knoppf  36501  f1omptsn  37303  mptsnun  37305  fin2so  37567  poimirlem27  37607  broucube  37614  ftc1anclem5  37657  ftc1anclem6  37658  sdclem2  37702  prdstotbnd  37754  prdsbnd2  37755  heiborlem10  37780  lshpkrcl  39072  tendoplcbv  40732  tendo0cbv  40743  tendoicbv  40750  lcfl7N  41458  lcf1o  41508  hdmap1cbv  41759  frlmsnic  42495  evlselv  42542  mzpclval  42681  mzpcompact2lem  42707  rmxyval  42872  dnnumch1  43001  aomclem3  43013  aomclem8  43018  dfac21  43023  pwfi2f1o  43053  dftrcl3  43682  dfrtrcl3  43695  rfovcnvf1od  43966  fsovrfovd  43971  fsovcnvlem  43975  dssmapnvod  43982  clsk3nimkb  44002  radcnvrat  44283  expgrowthi  44302  expgrowth  44304  dvradcnv2  44316  binomcxplemradcnv  44321  binomcxplemdvbinom  44322  binomcxplemdvsum  44324  binomcxplemnotnn0  44325  binomcxp  44326  wessf1ornlem  45092  projf1o  45104  fsumsermpt  45500  fmuldfeqlem1  45503  fprodcn  45521  sumnnodd  45551  limsupvaluz  45629  limsupvaluz2  45659  supcnvlimsup  45661  supcnvlimsupmpt  45662  liminfval2  45689  liminflelimsuplem  45696  fprodsubrecnncnv  45829  fprodaddrecnncnv  45831  dvsinax  45834  fperdvper  45840  dvcosax  45847  ioodvbdlimc1lem1  45852  ioodvbdlimc1  45854  ioodvbdlimc2  45856  dvnmul  45864  dvnprodlem1  45867  dvnprodlem2  45868  dvnprodlem3  45869  dvnprod  45870  itgsin0pilem1  45871  itgiccshift  45901  stoweidlem2  45923  stoweidlem17  45938  stoweidlem32  45953  stoweidlem34  45955  stoweidlem43  45964  stirlinglem2  45996  stirlinglem3  45997  stirlinglem8  46002  dirkerval  46012  dirkerval2  46015  dirkeritg  46023  dirkercncflem3  46026  dirkercncf  46028  fourierdlem14  46042  fourierdlem18  46046  fourierdlem53  46080  fourierdlem62  46089  fourierdlem71  46098  fourierdlem74  46101  fourierdlem75  46102  fourierdlem76  46103  fourierdlem80  46107  fourierdlem81  46108  fourierdlem84  46111  fourierdlem88  46115  fourierdlem92  46119  fourierdlem93  46120  fourierdlem94  46121  fourierdlem95  46122  fourierdlem96  46123  fourierdlem97  46124  fourierdlem98  46125  fourierdlem99  46126  fourierdlem101  46128  fourierdlem103  46130  fourierdlem104  46131  fourierdlem105  46132  fourierdlem106  46133  fourierdlem107  46134  fourierdlem108  46135  fourierdlem110  46137  fourierdlem111  46138  fourierdlem112  46139  fourierdlem113  46140  fourierdlem115  46142  fouriersw  46152  elaa2  46155  etransclem1  46156  etransclem5  46160  etransclem6  46161  etransclem11  46166  etransclem13  46168  etransclem41  46196  etransclem47  46202  etransc  46204  ioorrnopn  46226  ioorrnopnxr  46228  subsaliuncl  46279  sge0resplit  46327  sge0fodjrnlem  46337  nnfoctbdj  46377  iundjiun  46381  voliunsge0lem  46393  meaiuninclem  46401  meaiuninc  46402  meaiininclem  46407  meaiininc  46408  omeiunltfirp  46440  carageniuncllem2  46443  carageniuncl  46444  0ome  46450  isomennd  46452  hoicvrrex  46477  ovn0  46487  ovnsubaddlem2  46492  ovnsubadd  46493  sge0hsphoire  46510  hoidmv1lelem3  46514  hoidmv1le  46515  hoidmvlelem1  46516  hoidmvlelem2  46517  hoidmvlelem3  46518  hoidmvlelem4  46519  hoidmvlelem5  46520  hoidmvle  46521  ovnhoilem2  46523  ovnhoi  46524  hspmbllem2  46548  hspmbl  46550  hoimbl  46552  opnvonmbllem2  46554  ovnsubadd2  46567  ovolval4  46572  ovolval5lem3  46575  ovnovollem3  46579  iccvonmbl  46600  vonioolem2  46602  vonioo  46603  vonicclem2  46605  vonicc  46606  smflimlem4  46695  smfsuplem2  46733  smflimsuplem1  46741  smflimsuplem8  46748  smflimsup  46749  fundcmpsurbijinjpreimafv  47281  prproropf1o  47381  isuspgrim0  47756  uspgrimprop  47757  rmsupp0  48093  domnmsuppn0  48094  rmsuppss  48095  suppmptcfin  48104  ply1mulgsum  48119  lcoc0  48151  linc1  48154  lcoel0  48157  lcoss  48165  el0ldep  48195  lincresunit3  48210  isldepslvec2  48214  itcovalpclem2  48405  itcovalt2lem2  48410  amgmlemALT  48897