Theorem cbvmptv 5262

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 5264 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 2817	. . . 4 ⊢ (𝑥 = 𝑦 → (𝑥 ∈ 𝐴 ↔ 𝑦 ∈ 𝐴))
2		cbvmptv.1	. . . . 5 ⊢ (𝑥 = 𝑦 → 𝐵 = 𝐶)
3	2	eqeq2d 2744	. . . 4 ⊢ (𝑥 = 𝑦 → (𝑧 = 𝐵 ↔ 𝑧 = 𝐶))
4	1, 3	anbi12d 632	. . 3 ⊢ (𝑥 = 𝑦 → ((𝑥 ∈ 𝐴 ∧ 𝑧 = 𝐵) ↔ (𝑦 ∈ 𝐴 ∧ 𝑧 = 𝐶)))
5	4	cbvopab1v 5228	. 2 ⊢ {⟨𝑥, 𝑧⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑧 = 𝐵)} = {⟨𝑦, 𝑧⟩ ∣ (𝑦 ∈ 𝐴 ∧ 𝑧 = 𝐶)}
6		df-mpt 5233	. 2 ⊢ (𝑥 ∈ 𝐴 ↦ 𝐵) = {⟨𝑥, 𝑧⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑧 = 𝐵)}
7		df-mpt 5233	. 2 ⊢ (𝑦 ∈ 𝐴 ↦ 𝐶) = {⟨𝑦, 𝑧⟩ ∣ (𝑦 ∈ 𝐴 ∧ 𝑧 = 𝐶)}
8	5, 6, 7	3eqtr4i 2771	1 ⊢ (𝑥 ∈ 𝐴 ↦ 𝐵) = (𝑦 ∈ 𝐴 ↦ 𝐶)

Syntax hints:   → wi 4   ∧ wa 397   = wceq 1542   ∈ wcel 2107  {copab 5211   ↦ cmpt 5232

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 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-rab 3434  df-v 3477  df-dif 3952  df-un 3954  df-in 3956  df-ss 3966  df-nul 4324  df-if 4530  df-sn 4630  df-pr 4632  df-op 4636  df-opab 5212  df-mpt 5233

This theorem is referenced by:  fnmptfvd  7043  onnseq  8344  rdgsucmpt2  8430  frsucmpt2  8440  fsetfocdm  8855  fsetprcnex  8856  resixpfo  8930  pw2f1olem  9076  xpmapen  9145  dffi3  9426  ordtypecbv  9512  inf3lema  9619  cantnflem1  9684  cnfcomlem  9694  infxpenc2  10017  fseqenlem1  10019  dfac8a  10025  dfac12r  10141  r1om  10239  fictb  10240  cfsmo  10266  coftr  10268  fin23lem38  10344  compsscnv  10366  isf34lem1  10367  compss  10371  fin1a2lem1  10395  fin1a2lem3  10397  fin1a2lem13  10407  itunisuc  10414  hsmex  10427  domtriom  10438  axdc2  10444  zorn2g  10498  ttukey2g  10511  axdc  10516  konigth  10564  pwcfsdom  10578  canthp1  10649  wunex2  10733  wuncval2  10742  negiso  12194  infrenegsup  12197  rpnnen1  12967  caurcvg2  15624  caucvg  15625  summo  15663  zsum  15664  fsum  15666  ackbijnn  15774  prodmo  15880  zprod  15881  fprod  15885  iprodmul  15947  bpolyval  15993  phimullem  16712  eulerth  16716  iserodd  16768  prmreclem5  16853  prmrec  16855  vdwlem7  16920  vdwlem9  16922  vdwlem10  16923  ramub1  16961  ramcl  16962  yonedalem4c  18230  yonedalem3b  18232  gsumwspan  18727  smndex1iidm  18782  smndex1gid  18784  smndex2dlinvh  18798  grplactcnv  18926  galactghm  19272  symgfixfo  19307  pmtrdifwrdel  19353  pmtrdifwrdel2  19354  odf1o2  19441  sylow1lem2  19467  sylow1  19471  sylow2b  19491  sylow3lem1  19495  sylow3lem5  19499  sylow3  19501  efgtf  19590  efgsval  19599  ghmcyg  19764  cycsubgcyg  19769  ablfaclem3  19957  ablfac2  19959  srgbinomlem4  20052  fidomndrnglem  20925  isphld  21207  frlmphl  21336  mplmonmul  21591  evlslem2  21642  mat1ric  21989  mdetralt  22110  smadiadetlem3  22170  pmatcollpw3lem  22285  mp2pm2mplem5  22312  mp2pm2mp  22313  pm2mpmhmlem2  22321  cpmidpmat  22375  cpmadugsumlemF  22378  cpmadugsumfi  22379  cpmadumatpoly  22385  chcoeffeqlem  22387  cayleyhamilton0  22391  cayleyhamilton  22392  cayleyhamiltonALT  22393  cayleyhamilton1  22394  ordtbaslem  22692  ordtbas2  22695  lly1stc  23000  ptpjopn  23116  xkohmeo  23319  fbasrn  23388  elfm  23451  tmdmulg  23596  tmdgsum  23599  qustgpopn  23624  tsmsfbas  23632  tsmsf1o  23649  ustuqtoplem  23744  utopsnneip  23753  fmucnd  23797  ucnextcn  23809  met1stc  24030  prdsxmslem2  24038  metustto  24062  metustexhalf  24065  metuust  24069  cfilucfil2  24070  metuel  24073  metuel2  24074  psmetutop  24076  restmetu  24079  metucn  24080  xrge0tsms  24350  metdsge  24365  expcn  24388  pi1xfrcnv  24573  minveclem3b  24945  minveclem5  24950  minvec  24953  ovollb2  25006  ovolshftlem2  25027  ovolscalem2  25031  ovolicc  25040  ioombl1  25079  uniioombllem6  25105  volsup2  25122  vitali  25130  mbfi1fseq  25239  mbfmullem  25243  itg2seq  25260  itg2i1fseq  25273  itg2addlem  25276  itg2cnlem1  25279  itg2cn  25281  dvfsumrlimge0  25547  plyadd  25731  plymul  25732  coeeu  25739  coeid  25752  dvply2g  25798  plydivex  25810  elqaalem2  25833  elqaa  25835  taylthlem1  25885  taylth  25887  pserval  25922  radcnvlem2  25926  radcnvlt2  25931  dvradcnv  25933  pserulm  25934  psercn  25938  pserdvlem2  25940  pserdv  25941  efgh  26050  eff1olem  26057  circgrp  26061  circsubm  26062  logno1  26144  emcl  26507  harmonicbnd  26508  harmonicbnd2  26509  basel  26594  musum  26695  dchr1  26760  dchrptlem2  26768  dchrpt  26770  lgsqrlem4  26852  lgseisenlem3  26880  2sqlem1  26920  dchrmusumlema  26996  dchrmusum2  26997  dchrvmasumlema  27003  dchrvmasumiflem1  27004  dchrisum0ff  27010  dchrisum0lema  27017  dchrisum0lem1b  27018  dchrisum0lem2a  27020  nosupcbv  27205  noinfcbv  27220  precsexlemcbv  27655  wlknwwlksnbij  29173  clwlkclwwlken  29296  clwlknf1oclwwlkn  29368  frgrncvvdeqlem8  29590  frgrncvvdeqlem9  29591  numclwwlk1lem2  29644  ubthlem3  30156  minveco  30168  htth  30202  fsuppcurry1  31981  fsuppcurry2  31982  gsumhashmul  32239  xrge0tsmsd  32240  nsgmgc  32554  nsgqusf1olem1  32555  gicqusker  32564  lmicqusker  32566  ricqusker  32576  elrspunidl  32577  elrspunsn  32578  ply1degltdim  32739  lbsdiflsp0  32742  fedgmullem1  32745  fedgmul  32747  algextdeglem1  32803  madjusmdetlem2  32839  madjusmdet  32842  zartop  32887  zartopon  32888  zart0  32890  zarmxt1  32891  zarcmp  32893  rhmpreimacn  32896  xrge0mulc1cn  32952  xrge0tmd  32956  xrge0tmdALT  32957  gsumesum  33088  esumlub  33089  esumpcvgval  33107  esumcvg  33115  esumcvg2  33116  eulerpartlems  33390  eulerpart  33412  fibp1  33431  rrvadd  33482  ballotlemfval  33519  ballotlemi  33530  ballotlemsval  33538  ballotlemsv  33539  ballotlemsf1o  33543  ballotlemrval  33547  ballotlemrinv  33563  signsply0  33593  actfunsnf1o  33647  actfunsnrndisj  33648  itgexpif  33649  hgt750lemb  33699  derangfmla  34212  erdsze  34224  pconnpi1  34259  cvmscbv  34280  cvmsss2  34296  cvmliftlem15  34320  cvmlift2  34338  cvmlift3  34350  elmrsubrn  34542  iprodefisum  34742  gg-expcn  35195  knoppcnlem7  35423  knoppf  35459  f1omptsn  36266  mptsnun  36268  fin2so  36523  poimirlem27  36563  broucube  36570  ftc1anclem5  36613  ftc1anclem6  36614  sdclem2  36658  prdstotbnd  36710  prdsbnd2  36711  heiborlem10  36736  lshpkrcl  38034  tendoplcbv  39694  tendo0cbv  39705  tendoicbv  39712  lcfl7N  40420  lcf1o  40470  hdmap1cbv  40721  frlmsnic  41158  evlselv  41207  mzpclval  41511  mzpcompact2lem  41537  rmxyval  41702  dnnumch1  41834  aomclem3  41846  aomclem8  41851  dfac21  41856  pwfi2f1o  41886  dftrcl3  42519  dfrtrcl3  42532  rfovcnvf1od  42803  fsovrfovd  42808  fsovcnvlem  42812  dssmapnvod  42819  clsk3nimkb  42839  radcnvrat  43121  expgrowthi  43140  expgrowth  43142  dvradcnv2  43154  binomcxplemradcnv  43159  binomcxplemdvbinom  43160  binomcxplemdvsum  43162  binomcxplemnotnn0  43163  binomcxp  43164  wessf1ornlem  43930  projf1o  43944  fsumsermpt  44343  fmuldfeqlem1  44346  fprodcn  44364  sumnnodd  44394  limsupvaluz  44472  limsupvaluz2  44502  supcnvlimsup  44504  supcnvlimsupmpt  44505  liminfval2  44532  liminflelimsuplem  44539  fprodsubrecnncnv  44672  fprodaddrecnncnv  44674  dvsinax  44677  fperdvper  44683  dvcosax  44690  ioodvbdlimc1lem1  44695  ioodvbdlimc1  44697  ioodvbdlimc2  44699  dvnmul  44707  dvnprodlem1  44710  dvnprodlem2  44711  dvnprodlem3  44712  dvnprod  44713  itgsin0pilem1  44714  itgiccshift  44744  stoweidlem2  44766  stoweidlem17  44781  stoweidlem32  44796  stoweidlem34  44798  stoweidlem43  44807  stirlinglem2  44839  stirlinglem3  44840  stirlinglem8  44845  dirkerval  44855  dirkerval2  44858  dirkeritg  44866  dirkercncflem3  44869  dirkercncf  44871  fourierdlem14  44885  fourierdlem18  44889  fourierdlem53  44923  fourierdlem62  44932  fourierdlem71  44941  fourierdlem74  44944  fourierdlem75  44945  fourierdlem76  44946  fourierdlem80  44950  fourierdlem81  44951  fourierdlem84  44954  fourierdlem88  44958  fourierdlem92  44962  fourierdlem93  44963  fourierdlem94  44964  fourierdlem95  44965  fourierdlem96  44966  fourierdlem97  44967  fourierdlem98  44968  fourierdlem99  44969  fourierdlem101  44971  fourierdlem103  44973  fourierdlem104  44974  fourierdlem105  44975  fourierdlem106  44976  fourierdlem107  44977  fourierdlem108  44978  fourierdlem110  44980  fourierdlem111  44981  fourierdlem112  44982  fourierdlem113  44983  fourierdlem115  44985  fouriersw  44995  elaa2  44998  etransclem1  44999  etransclem5  45003  etransclem6  45004  etransclem11  45009  etransclem13  45011  etransclem41  45039  etransclem47  45045  etransc  45047  ioorrnopn  45069  ioorrnopnxr  45071  subsaliuncl  45122  sge0resplit  45170  sge0fodjrnlem  45180  nnfoctbdj  45220  iundjiun  45224  voliunsge0lem  45236  meaiuninclem  45244  meaiuninc  45245  meaiininclem  45250  meaiininc  45251  omeiunltfirp  45283  carageniuncllem2  45286  carageniuncl  45287  0ome  45293  isomennd  45295  hoicvrrex  45320  ovn0  45330  ovnsubaddlem2  45335  ovnsubadd  45336  sge0hsphoire  45353  hoidmv1lelem3  45357  hoidmv1le  45358  hoidmvlelem1  45359  hoidmvlelem2  45360  hoidmvlelem3  45361  hoidmvlelem4  45362  hoidmvlelem5  45363  hoidmvle  45364  ovnhoilem2  45366  ovnhoi  45367  hspmbllem2  45391  hspmbl  45393  hoimbl  45395  opnvonmbllem2  45397  ovnsubadd2  45410  ovolval4  45415  ovolval5lem3  45418  ovnovollem3  45422  iccvonmbl  45443  vonioolem2  45445  vonioo  45446  vonicclem2  45448  vonicc  45449  smflimlem4  45538  smfsuplem2  45576  smflimsuplem1  45584  smflimsuplem8  45591  smflimsup  45592  fundcmpsurbijinjpreimafv  46123  prproropf1o  46223  funcrngcsetcALT  46945  rmsupp0  47092  domnmsuppn0  47093  rmsuppss  47094  suppmptcfin  47103  ply1mulgsum  47119  lcoc0  47151  linc1  47154  lcoel0  47157  lcoss  47165  el0ldep  47195  lincresunit3  47210  isldepslvec2  47214  itcovalpclem2  47405  itcovalt2lem2  47410  amgmlemALT  47898