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  27652  wlknwwlksnbij  29142  clwlkclwwlken  29265  clwlknf1oclwwlkn  29337  frgrncvvdeqlem8  29559  frgrncvvdeqlem9  29560  numclwwlk1lem2  29613  ubthlem3  30125  minveco  30137  htth  30171  fsuppcurry1  31950  fsuppcurry2  31951  gsumhashmul  32208  xrge0tsmsd  32209  nsgmgc  32523  nsgqusf1olem1  32524  gicqusker  32533  lmicqusker  32535  ricqusker  32545  elrspunidl  32546  elrspunsn  32547  ply1degltdim  32708  lbsdiflsp0  32711  fedgmullem1  32714  fedgmul  32716  algextdeglem1  32772  madjusmdetlem2  32808  madjusmdet  32811  zartop  32856  zartopon  32857  zart0  32859  zarmxt1  32860  zarcmp  32862  rhmpreimacn  32865  xrge0mulc1cn  32921  xrge0tmd  32925  xrge0tmdALT  32926  gsumesum  33057  esumlub  33058  esumpcvgval  33076  esumcvg  33084  esumcvg2  33085  eulerpartlems  33359  eulerpart  33381  fibp1  33400  rrvadd  33451  ballotlemfval  33488  ballotlemi  33499  ballotlemsval  33507  ballotlemsv  33508  ballotlemsf1o  33512  ballotlemrval  33516  ballotlemrinv  33532  signsply0  33562  actfunsnf1o  33616  actfunsnrndisj  33617  itgexpif  33618  hgt750lemb  33668  derangfmla  34181  erdsze  34193  pconnpi1  34228  cvmscbv  34249  cvmsss2  34265  cvmliftlem15  34289  cvmlift2  34307  cvmlift3  34319  elmrsubrn  34511  iprodefisum  34711  gg-expcn  35164  knoppcnlem7  35375  knoppf  35411  f1omptsn  36218  mptsnun  36220  fin2so  36475  poimirlem27  36515  broucube  36522  ftc1anclem5  36565  ftc1anclem6  36566  sdclem2  36610  prdstotbnd  36662  prdsbnd2  36663  heiborlem10  36688  lshpkrcl  37986  tendoplcbv  39646  tendo0cbv  39657  tendoicbv  39664  lcfl7N  40372  lcf1o  40422  hdmap1cbv  40673  frlmsnic  41110  evlselv  41159  mzpclval  41463  mzpcompact2lem  41489  rmxyval  41654  dnnumch1  41786  aomclem3  41798  aomclem8  41803  dfac21  41808  pwfi2f1o  41838  dftrcl3  42471  dfrtrcl3  42484  rfovcnvf1od  42755  fsovrfovd  42760  fsovcnvlem  42764  dssmapnvod  42771  clsk3nimkb  42791  radcnvrat  43073  expgrowthi  43092  expgrowth  43094  dvradcnv2  43106  binomcxplemradcnv  43111  binomcxplemdvbinom  43112  binomcxplemdvsum  43114  binomcxplemnotnn0  43115  binomcxp  43116  wessf1ornlem  43882  projf1o  43896  fsumsermpt  44295  fmuldfeqlem1  44298  fprodcn  44316  sumnnodd  44346  limsupvaluz  44424  limsupvaluz2  44454  supcnvlimsup  44456  supcnvlimsupmpt  44457  liminfval2  44484  liminflelimsuplem  44491  fprodsubrecnncnv  44624  fprodaddrecnncnv  44626  dvsinax  44629  fperdvper  44635  dvcosax  44642  ioodvbdlimc1lem1  44647  ioodvbdlimc1  44649  ioodvbdlimc2  44651  dvnmul  44659  dvnprodlem1  44662  dvnprodlem2  44663  dvnprodlem3  44664  dvnprod  44665  itgsin0pilem1  44666  itgiccshift  44696  stoweidlem2  44718  stoweidlem17  44733  stoweidlem32  44748  stoweidlem34  44750  stoweidlem43  44759  stirlinglem2  44791  stirlinglem3  44792  stirlinglem8  44797  dirkerval  44807  dirkerval2  44810  dirkeritg  44818  dirkercncflem3  44821  dirkercncf  44823  fourierdlem14  44837  fourierdlem18  44841  fourierdlem53  44875  fourierdlem62  44884  fourierdlem71  44893  fourierdlem74  44896  fourierdlem75  44897  fourierdlem76  44898  fourierdlem80  44902  fourierdlem81  44903  fourierdlem84  44906  fourierdlem88  44910  fourierdlem92  44914  fourierdlem93  44915  fourierdlem94  44916  fourierdlem95  44917  fourierdlem96  44918  fourierdlem97  44919  fourierdlem98  44920  fourierdlem99  44921  fourierdlem101  44923  fourierdlem103  44925  fourierdlem104  44926  fourierdlem105  44927  fourierdlem106  44928  fourierdlem107  44929  fourierdlem108  44930  fourierdlem110  44932  fourierdlem111  44933  fourierdlem112  44934  fourierdlem113  44935  fourierdlem115  44937  fouriersw  44947  elaa2  44950  etransclem1  44951  etransclem5  44955  etransclem6  44956  etransclem11  44961  etransclem13  44963  etransclem41  44991  etransclem47  44997  etransc  44999  ioorrnopn  45021  ioorrnopnxr  45023  subsaliuncl  45074  sge0resplit  45122  sge0fodjrnlem  45132  nnfoctbdj  45172  iundjiun  45176  voliunsge0lem  45188  meaiuninclem  45196  meaiuninc  45197  meaiininclem  45202  meaiininc  45203  omeiunltfirp  45235  carageniuncllem2  45238  carageniuncl  45239  0ome  45245  isomennd  45247  hoicvrrex  45272  ovn0  45282  ovnsubaddlem2  45287  ovnsubadd  45288  sge0hsphoire  45305  hoidmv1lelem3  45309  hoidmv1le  45310  hoidmvlelem1  45311  hoidmvlelem2  45312  hoidmvlelem3  45313  hoidmvlelem4  45314  hoidmvlelem5  45315  hoidmvle  45316  ovnhoilem2  45318  ovnhoi  45319  hspmbllem2  45343  hspmbl  45345  hoimbl  45347  opnvonmbllem2  45349  ovnsubadd2  45362  ovolval4  45367  ovolval5lem3  45370  ovnovollem3  45374  iccvonmbl  45395  vonioolem2  45397  vonioo  45398  vonicclem2  45400  vonicc  45401  smflimlem4  45490  smfsuplem2  45528  smflimsuplem1  45536  smflimsuplem8  45543  smflimsup  45544  fundcmpsurbijinjpreimafv  46075  prproropf1o  46175  funcrngcsetcALT  46897  rmsupp0  47044  domnmsuppn0  47045  rmsuppss  47046  suppmptcfin  47055  ply1mulgsum  47071  lcoc0  47103  linc1  47106  lcoel0  47109  lcoss  47117  el0ldep  47147  lincresunit3  47162  isldepslvec2  47166  itcovalpclem2  47357  itcovalt2lem2  47362  amgmlemALT  47850