Theorem cbvmptv 5254

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 5256 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 2815	. . . 4 ⊢ (𝑥 = 𝑦 → (𝑥 ∈ 𝐴 ↔ 𝑦 ∈ 𝐴))
2		cbvmptv.1	. . . . 5 ⊢ (𝑥 = 𝑦 → 𝐵 = 𝐶)
3	2	eqeq2d 2742	. . . 4 ⊢ (𝑥 = 𝑦 → (𝑧 = 𝐵 ↔ 𝑧 = 𝐶))
4	1, 3	anbi12d 631	. . 3 ⊢ (𝑥 = 𝑦 → ((𝑥 ∈ 𝐴 ∧ 𝑧 = 𝐵) ↔ (𝑦 ∈ 𝐴 ∧ 𝑧 = 𝐶)))
5	4	cbvopab1v 5220	. 2 ⊢ {⟨𝑥, 𝑧⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑧 = 𝐵)} = {⟨𝑦, 𝑧⟩ ∣ (𝑦 ∈ 𝐴 ∧ 𝑧 = 𝐶)}
6		df-mpt 5225	. 2 ⊢ (𝑥 ∈ 𝐴 ↦ 𝐵) = {⟨𝑥, 𝑧⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑧 = 𝐵)}
7		df-mpt 5225	. 2 ⊢ (𝑦 ∈ 𝐴 ↦ 𝐶) = {⟨𝑦, 𝑧⟩ ∣ (𝑦 ∈ 𝐴 ∧ 𝑧 = 𝐶)}
8	5, 6, 7	3eqtr4i 2769	1 ⊢ (𝑥 ∈ 𝐴 ↦ 𝐵) = (𝑦 ∈ 𝐴 ↦ 𝐶)

Syntax hints:   → wi 4   ∧ wa 396   = wceq 1541   ∈ wcel 2106  {copab 5203   ↦ cmpt 5224

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2702

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-sb 2068  df-clab 2709  df-cleq 2723  df-clel 2809  df-rab 3432  df-v 3475  df-dif 3947  df-un 3949  df-in 3951  df-ss 3961  df-nul 4319  df-if 4523  df-sn 4623  df-pr 4625  df-op 4629  df-opab 5204  df-mpt 5225

This theorem is referenced by:  fnmptfvd  7027  onnseq  8326  rdgsucmpt2  8412  frsucmpt2  8422  fsetfocdm  8838  fsetprcnex  8839  resixpfo  8913  pw2f1olem  9059  xpmapen  9128  dffi3  9408  ordtypecbv  9494  inf3lema  9601  cantnflem1  9666  cnfcomlem  9676  infxpenc2  9999  fseqenlem1  10001  dfac8a  10007  dfac12r  10123  r1om  10221  fictb  10222  cfsmo  10248  coftr  10250  fin23lem38  10326  compsscnv  10348  isf34lem1  10349  compss  10353  fin1a2lem1  10377  fin1a2lem3  10379  fin1a2lem13  10389  itunisuc  10396  hsmex  10409  domtriom  10420  axdc2  10426  zorn2g  10480  ttukey2g  10493  axdc  10498  konigth  10546  pwcfsdom  10560  canthp1  10631  wunex2  10715  wuncval2  10724  negiso  12176  infrenegsup  12179  rpnnen1  12949  caurcvg2  15606  caucvg  15607  summo  15645  zsum  15646  fsum  15648  ackbijnn  15756  prodmo  15862  zprod  15863  fprod  15867  iprodmul  15929  bpolyval  15975  phimullem  16694  eulerth  16698  iserodd  16750  prmreclem5  16835  prmrec  16837  vdwlem7  16902  vdwlem9  16904  vdwlem10  16905  ramub1  16943  ramcl  16944  yonedalem4c  18212  yonedalem3b  18214  gsumwspan  18702  smndex1iidm  18757  smndex1gid  18759  smndex2dlinvh  18773  grplactcnv  18900  galactghm  19236  symgfixfo  19271  pmtrdifwrdel  19317  pmtrdifwrdel2  19318  odf1o2  19405  sylow1lem2  19431  sylow1  19435  sylow2b  19455  sylow3lem1  19459  sylow3lem5  19463  sylow3  19465  efgtf  19554  efgsval  19563  ghmcyg  19723  cycsubgcyg  19728  ablfaclem3  19916  ablfac2  19918  srgbinomlem4  20010  fidomndrnglem  20859  isphld  21140  frlmphl  21269  mplmonmul  21519  evlslem2  21571  mat1ric  21918  mdetralt  22039  smadiadetlem3  22099  pmatcollpw3lem  22214  mp2pm2mplem5  22241  mp2pm2mp  22242  pm2mpmhmlem2  22250  cpmidpmat  22304  cpmadugsumlemF  22307  cpmadugsumfi  22308  cpmadumatpoly  22314  chcoeffeqlem  22316  cayleyhamilton0  22320  cayleyhamilton  22321  cayleyhamiltonALT  22322  cayleyhamilton1  22323  ordtbaslem  22621  ordtbas2  22624  lly1stc  22929  ptpjopn  23045  xkohmeo  23248  fbasrn  23317  elfm  23380  tmdmulg  23525  tmdgsum  23528  qustgpopn  23553  tsmsfbas  23561  tsmsf1o  23578  ustuqtoplem  23673  utopsnneip  23682  fmucnd  23726  ucnextcn  23738  met1stc  23959  prdsxmslem2  23967  metustto  23991  metustexhalf  23994  metuust  23998  cfilucfil2  23999  metuel  24002  metuel2  24003  psmetutop  24005  restmetu  24008  metucn  24009  xrge0tsms  24279  metdsge  24294  expcn  24317  pi1xfrcnv  24502  minveclem3b  24874  minveclem5  24879  minvec  24882  ovollb2  24935  ovolshftlem2  24956  ovolscalem2  24960  ovolicc  24969  ioombl1  25008  uniioombllem6  25034  volsup2  25051  vitali  25059  mbfi1fseq  25168  mbfmullem  25172  itg2seq  25189  itg2i1fseq  25202  itg2addlem  25205  itg2cnlem1  25208  itg2cn  25210  dvfsumrlimge0  25476  plyadd  25660  plymul  25661  coeeu  25668  coeid  25681  dvply2g  25727  plydivex  25739  elqaalem2  25762  elqaa  25764  taylthlem1  25814  taylth  25816  pserval  25851  radcnvlem2  25855  radcnvlt2  25860  dvradcnv  25862  pserulm  25863  psercn  25867  pserdvlem2  25869  pserdv  25870  efgh  25979  eff1olem  25986  circgrp  25990  circsubm  25991  logno1  26073  emcl  26434  harmonicbnd  26435  harmonicbnd2  26436  basel  26521  musum  26622  dchr1  26687  dchrptlem2  26695  dchrpt  26697  lgsqrlem4  26779  lgseisenlem3  26807  2sqlem1  26847  dchrmusumlema  26923  dchrmusum2  26924  dchrvmasumlema  26930  dchrvmasumiflem1  26931  dchrisum0ff  26937  dchrisum0lema  26944  dchrisum0lem1b  26945  dchrisum0lem2a  26947  nosupcbv  27132  noinfcbv  27147  wlknwwlksnbij  29007  clwlkclwwlken  29130  clwlknf1oclwwlkn  29202  frgrncvvdeqlem8  29424  frgrncvvdeqlem9  29425  numclwwlk1lem2  29478  ubthlem3  29988  minveco  30000  htth  30034  fsuppcurry1  31821  fsuppcurry2  31822  gsumhashmul  32079  xrge0tsmsd  32080  nsgmgc  32379  nsgqusf1olem1  32380  gicqusker  32388  lmicqusker  32390  ricqusker  32396  elrspunidl  32397  elrspunsn  32398  ply1degltdim  32546  lbsdiflsp0  32549  fedgmullem1  32552  fedgmul  32554  madjusmdetlem2  32639  madjusmdet  32642  zartop  32687  zartopon  32688  zart0  32690  zarmxt1  32691  zarcmp  32693  rhmpreimacn  32696  xrge0mulc1cn  32752  xrge0tmd  32756  xrge0tmdALT  32757  gsumesum  32888  esumlub  32889  esumpcvgval  32907  esumcvg  32915  esumcvg2  32916  eulerpartlems  33190  eulerpart  33212  fibp1  33231  rrvadd  33282  ballotlemfval  33319  ballotlemi  33330  ballotlemsval  33338  ballotlemsv  33339  ballotlemsf1o  33343  ballotlemrval  33347  ballotlemrinv  33363  signsply0  33393  actfunsnf1o  33447  actfunsnrndisj  33448  itgexpif  33449  hgt750lemb  33499  derangfmla  34012  erdsze  34024  pconnpi1  34059  cvmscbv  34080  cvmsss2  34096  cvmliftlem15  34120  cvmlift2  34138  cvmlift3  34150  elmrsubrn  34342  iprodefisum  34541  knoppcnlem7  35179  knoppf  35215  f1omptsn  36022  mptsnun  36024  fin2so  36279  poimirlem27  36319  broucube  36326  ftc1anclem5  36369  ftc1anclem6  36370  sdclem2  36415  prdstotbnd  36467  prdsbnd2  36468  heiborlem10  36493  lshpkrcl  37791  tendoplcbv  39451  tendo0cbv  39462  tendoicbv  39469  lcfl7N  40177  lcf1o  40227  hdmap1cbv  40478  frlmsnic  40914  mzpclval  41234  mzpcompact2lem  41260  rmxyval  41425  dnnumch1  41557  aomclem3  41569  aomclem8  41574  dfac21  41579  pwfi2f1o  41609  dftrcl3  42242  dfrtrcl3  42255  rfovcnvf1od  42526  fsovrfovd  42531  fsovcnvlem  42535  dssmapnvod  42542  clsk3nimkb  42562  radcnvrat  42844  expgrowthi  42863  expgrowth  42865  dvradcnv2  42877  binomcxplemradcnv  42882  binomcxplemdvbinom  42883  binomcxplemdvsum  42885  binomcxplemnotnn0  42886  binomcxp  42887  wessf1ornlem  43653  projf1o  43667  fsumsermpt  44068  fmuldfeqlem1  44071  fprodcn  44089  sumnnodd  44119  limsupvaluz  44197  limsupvaluz2  44227  supcnvlimsup  44229  supcnvlimsupmpt  44230  liminfval2  44257  liminflelimsuplem  44264  fprodsubrecnncnv  44397  fprodaddrecnncnv  44399  dvsinax  44402  fperdvper  44408  dvcosax  44415  ioodvbdlimc1lem1  44420  ioodvbdlimc1  44422  ioodvbdlimc2  44424  dvnmul  44432  dvnprodlem1  44435  dvnprodlem2  44436  dvnprodlem3  44437  dvnprod  44438  itgsin0pilem1  44439  itgiccshift  44469  stoweidlem2  44491  stoweidlem17  44506  stoweidlem32  44521  stoweidlem34  44523  stoweidlem43  44532  stirlinglem2  44564  stirlinglem3  44565  stirlinglem8  44570  dirkerval  44580  dirkerval2  44583  dirkeritg  44591  dirkercncflem3  44594  dirkercncf  44596  fourierdlem14  44610  fourierdlem18  44614  fourierdlem53  44648  fourierdlem62  44657  fourierdlem71  44666  fourierdlem74  44669  fourierdlem75  44670  fourierdlem76  44671  fourierdlem80  44675  fourierdlem81  44676  fourierdlem84  44679  fourierdlem88  44683  fourierdlem92  44687  fourierdlem93  44688  fourierdlem94  44689  fourierdlem95  44690  fourierdlem96  44691  fourierdlem97  44692  fourierdlem98  44693  fourierdlem99  44694  fourierdlem101  44696  fourierdlem103  44698  fourierdlem104  44699  fourierdlem105  44700  fourierdlem106  44701  fourierdlem107  44702  fourierdlem108  44703  fourierdlem110  44705  fourierdlem111  44706  fourierdlem112  44707  fourierdlem113  44708  fourierdlem115  44710  fouriersw  44720  elaa2  44723  etransclem1  44724  etransclem5  44728  etransclem6  44729  etransclem11  44734  etransclem13  44736  etransclem41  44764  etransclem47  44770  etransc  44772  ioorrnopn  44794  ioorrnopnxr  44796  subsaliuncl  44847  sge0resplit  44895  sge0fodjrnlem  44905  nnfoctbdj  44945  iundjiun  44949  voliunsge0lem  44961  meaiuninclem  44969  meaiuninc  44970  meaiininclem  44975  meaiininc  44976  omeiunltfirp  45008  carageniuncllem2  45011  carageniuncl  45012  0ome  45018  isomennd  45020  hoicvrrex  45045  ovn0  45055  ovnsubaddlem2  45060  ovnsubadd  45061  sge0hsphoire  45078  hoidmv1lelem3  45082  hoidmv1le  45083  hoidmvlelem1  45084  hoidmvlelem2  45085  hoidmvlelem3  45086  hoidmvlelem4  45087  hoidmvlelem5  45088  hoidmvle  45089  ovnhoilem2  45091  ovnhoi  45092  hspmbllem2  45116  hspmbl  45118  hoimbl  45120  opnvonmbllem2  45122  ovnsubadd2  45135  ovolval4  45140  ovolval5lem3  45143  ovnovollem3  45147  iccvonmbl  45168  vonioolem2  45170  vonioo  45171  vonicclem2  45173  vonicc  45174  smflimlem4  45263  smfsuplem2  45301  smflimsuplem1  45309  smflimsuplem8  45316  smflimsup  45317  fundcmpsurbijinjpreimafv  45847  prproropf1o  45947  funcrngcsetcALT  46545  rmsupp0  46692  domnmsuppn0  46693  rmsuppss  46694  suppmptcfin  46703  ply1mulgsum  46719  lcoc0  46751  linc1  46754  lcoel0  46757  lcoss  46765  el0ldep  46795  lincresunit3  46810  isldepslvec2  46814  itcovalpclem2  47005  itcovalt2lem2  47010  amgmlemALT  47498