Theorem cbvmptv 5209

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 5210 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 2844	. . . 4 ⊢ (𝑥 = 𝑦 → (𝑥 ∈ 𝐴 ↔ 𝑦 ∈ 𝐴))
2		cbvmptv.1	. . . . 5 ⊢ (𝑥 = 𝑦 → 𝐵 = 𝐶)
3	2	eqeq2d 2772	. . . 4 ⊢ (𝑥 = 𝑦 → (𝑧 = 𝐵 ↔ 𝑧 = 𝐶))
4	1, 3	anbi12d 644	. . 3 ⊢ (𝑥 = 𝑦 → ((𝑥 ∈ 𝐴 ∧ 𝑧 = 𝐵) ↔ (𝑦 ∈ 𝐴 ∧ 𝑧 = 𝐶)))
5	4	cbvopab1v 5183	. 2 ⊢ {⟨𝑥, 𝑧⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑧 = 𝐵)} = {⟨𝑦, 𝑧⟩ ∣ (𝑦 ∈ 𝐴 ∧ 𝑧 = 𝐶)}
6		df-mpt 5187	. 2 ⊢ (𝑥 ∈ 𝐴 ↦ 𝐵) = {⟨𝑥, 𝑧⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑧 = 𝐵)}
7		df-mpt 5187	. 2 ⊢ (𝑦 ∈ 𝐴 ↦ 𝐶) = {⟨𝑦, 𝑧⟩ ∣ (𝑦 ∈ 𝐴 ∧ 𝑧 = 𝐶)}
8	5, 6, 7	3eqtr4i 2794	1 ⊢ (𝑥 ∈ 𝐴 ↦ 𝐵) = (𝑦 ∈ 𝐴 ↦ 𝐶)

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   = wceq 1570   ∈ wcel 2145  {copab 5167   ↦ cmpt 5186

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2733

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-clab 2740  df-cleq 2753  df-clel 2836  df-rab 3414  df-v 3453  df-dif 3902  df-un 3904  df-ss 3916  df-nul 4280  df-if 4483  df-sn 4585  df-pr 4587  df-op 4591  df-opab 5168  df-mpt 5187

This theorem is used by:  fnmptfvd  7032  mptcnfimad  7987  onnseq  8336  rdgsucmpt2  8422  frsucmpt2  8432  fsetfocdm  8867  fsetprcnex  8868  resixpfo  8948  pw2f1olem  9084  xpmapen  9148  dffi3  9407  ordtypecbv  9495  inf3lema  9609  cantnflem1  9674  cnfcomlem  9684  infxpenc2  10082  fseqenlem1  10084  dfac8a  10090  dfac12r  10206  hfom  10302  fictb  10303  cfsmo  10330  coftr  10332  fin23lem38  10408  compsscnv  10430  isf34lem1  10431  compss  10435  fin1a2lem1  10459  fin1a2lem3  10461  fin1a2lem13  10471  itunisuc  10478  hsmex  10491  domtriom  10502  axdc2  10508  zorn2g  10562  ttukey2g  10575  axdc  10580  konigth  10635  pwcfsdom  10649  canthp1  10720  wunex2  10804  wuncval2  10813  negiso  12278  infrenegsup  12281  rpnnen1  13092  caurcvg2  15825  caucvg  15826  summo  15863  zsum  15864  fsum  15866  ackbijnn  15977  cbvprodv  16063  prodmo  16083  zprod  16084  fprod  16088  iprodmul  16150  bpolyval  16195  phimullem  16936  eulerth  16940  iserodd  16993  prmreclem5  17078  prmrec  17080  vdwlem7  17145  vdwlem9  17147  vdwlem10  17148  ramub1  17186  ramcl  17187  yonedalem4c  18431  yonedalem3b  18433  gsumwspan  19022  smndex1iidm  19077  smndex1gid  19080  smndex1gidOLD  19081  smndex2dlinvh  19096  grplactcnv  19233  gicqusker  19482  galactghm  19598  symgfixfo  19633  pmtrdifwrdel  19679  pmtrdifwrdel2  19680  odf1o2  19767  sylow1lem2  19793  sylow1  19797  sylow2b  19817  sylow3lem1  19821  sylow3lem5  19825  sylow3  19827  efgtf  19916  efgsval  19925  ghmcyg  20090  cycsubgcyg  20095  ablfaclem3  20283  ablfac2  20285  srgbinomlem4  20435  funcrngcsetcALT  20873  fidomndrnglem  21010  isphld  21940  frlmphl  22067  mplmonmul  22325  evlslem2  22368  mat1ric  22782  mdetralt  22903  smadiadetlem3  22963  pmatcollpw3lem  23081  mp2pm2mplem5  23108  mp2pm2mp  23109  pm2mpmhmlem2  23117  cpmidpmat  23171  cpmadugsumlemF  23174  cpmadugsumfi  23175  cpmadumatpoly  23181  chcoeffeqlem  23183  cayleyhamilton0  23187  cayleyhamilton  23188  cayleyhamiltonALT  23189  cayleyhamilton1  23190  ordtbaslem  23486  ordtbas2  23489  lly1stc  23795  ptpjopn  23911  xkohmeo  24114  fbasrn  24183  elfm  24246  tmdmulg  24391  tmdgsum  24394  qustgpopn  24419  tsmsfbas  24427  tsmsf1o  24444  ustuqtoplem  24538  utopsnneip  24547  fmucnd  24590  ucnextcn  24602  met1stc  24820  prdsxmslem2  24828  metustto  24852  metustexhalf  24855  metuust  24859  cfilucfil2  24860  metuel  24863  metuel2  24864  psmetutop  24866  restmetu  24869  metucn  24870  xrge0tsms  25134  metdsge  25149  expcn  25173  pi1xfrcnv  25358  minveclem3b  25729  minveclem5  25734  minvec  25737  ovollb2  25790  ovolshftlem2  25811  ovolscalem2  25815  ovolicc  25824  ioombl1  25863  uniioombllem6  25889  volsup2  25906  vitali  25914  mbfi1fseq  26022  mbfmullem  26026  itg2seq  26043  itg2i1fseq  26056  itg2addlem  26059  itg2cnlem1  26062  itg2cn  26064  cbvitgv  26077  dvfsumrlimge0  26330  plyadd  26516  plymul  26517  coeeu  26524  coeid  26537  dvply2g  26588  plydivex  26600  elqaalem2  26625  elqaa  26627  taylthlem1  26682  taylth  26684  pserval  26719  radcnvlem2  26723  radcnvlt2  26728  dvradcnv  26730  pserulm  26731  psercn  26735  pserdvlem2  26737  pserdv  26738  efgh  26851  eff1olem  26858  circgrp  26862  circsubm  26863  logno1  26946  emcl  27312  harmonicbnd  27313  harmonicbnd2  27314  basel  27399  musum  27500  dchr1  27566  dchrptlem2  27574  dchrpt  27576  lgsqrlem4  27658  lgseisenlem3  27686  2sqlem1  27726  dchrmusumlema  27802  dchrmusum2  27803  dchrvmasumlema  27809  dchrvmasumiflem1  27810  dchrisum0ff  27816  dchrisum0lema  27823  dchrisum0lem1b  27824  dchrisum0lem2a  27826  nosupcbv  28041  noinfcbv  28056  precsexlemcbv  28574  seqsfn  28677  seqsp1  28679  wlknwwlksnbij  30459  clwlkclwwlken  30585  clwlknf1oclwwlkn  30657  frgrncvvdeqlem8  30889  frgrncvvdeqlem9  30890  numclwwlk1lem2  30943  ubthlem3  31456  minveco  31468  htth  31502  fsuppcurry1  33298  fsuppcurry2  33299  gsumhashmul  33610  gsummulsubdishift1  33611  gsummulsubdishift1s  33613  gsummulsubdishift2s  33614  xrge0tsmsd  33616  elrgspnlem1  33785  elrgspnlem2  33786  elrgspn  33789  elrgspnsubrunlem1  33790  elrgspnsubrunlem2  33791  elrgspnsubrun  33792  idomsubr  33853  nsgmgc  33945  nsgqusf1olem1  33946  lmicqusker  33951  ricqusker  33959  elrspunidl  33960  elrspunsn  33961  zringfrac  34068  0mplric  34129  selvply1rhmlemb  34133  selvply1rhmlem3  34136  selvply1rhmlem5  34138  selvply1rhm  34139  mplidom  34142  mplvrpmga  34159  mplvrpmrhm  34161  psrgsum  34162  psrmonmul  34164  psrmonprod  34166  splysubrg  34174  issply  34175  esplyfvaln  34188  vietalem  34193  vieta  34194  ply1degltdim  34237  lbsdiflsp0  34240  fedgmullem1  34243  fedgmul  34245  assarrginv  34250  evls1fldgencl  34284  fldextrspunlsplem  34287  fldextrspunlsp  34288  extdgfialglem2  34307  extdgfialg  34308  algextdeglem4  34334  algextdeg  34339  constrcbvlem  34369  madjusmdetlem2  34442  madjusmdet  34445  zartop  34490  zartopon  34491  zart0  34493  zarmxt1  34494  zarcmp  34496  rhmpreimacn  34499  xrge0mulc1cn  34555  xrge0tmd  34559  xrge0tmdALT  34560  cbvesumv  34657  gsumesum  34673  esumlub  34674  esumpcvgval  34692  esumcvg  34700  esumcvg2  34701  eulerpartlems  34975  eulerpart  34997  fibp1  35016  rrvadd  35067  ballotlemfval  35105  ballotlemi  35116  ballotlemsval  35124  ballotlemsv  35125  ballotlemsf1o  35129  ballotlemrval  35133  ballotlemrinv  35149  signsply0  35163  actfunsnf1o  35216  actfunsnrndisj  35217  itgexpif  35218  hgt750lemb  35268  onvf1odlem3  35857  derangfmla  35924  erdsze  35936  pconnpi1  35971  cvmscbv  35992  cvmsss2  36008  cvmliftlem15  36032  cvmlift2  36050  cvmlift3  36062  elmrsubrn  36254  iprodefisum  36475  cbvprodvw2  37006  cbvitgvw2  37007  knoppcnlem7  37335  knoppf  37371  f1omptsn  38228  mptsnun  38230  fin2so  38498  poimirlem27  38533  broucube  38540  ftc1anclem5  38583  ftc1anclem6  38584  sdclem2  38644  prdstotbnd  38696  prdsbnd2  38697  heiborlem10  38722  lshpkrcl  40141  tendoplcbv  41800  tendo0cbv  41811  tendoicbv  41818  lcfl7N  42526  lcf1o  42576  hdmap1cbv  42827  frlmsnic  43566  evlselv  43579  mzpclval  43689  mzpcompact2lem  43715  rmxyval  43875  dnnumch1  44004  aomclem3  44016  aomclem8  44021  dfac21  44026  pwfi2f1o  44056  dftrcl3  44679  dfrtrcl3  44692  rfovcnvf1od  44963  fsovrfovd  44968  fsovcnvlem  44972  dssmapnvod  44979  clsk3nimkb  44999  radcnvrat  45257  expgrowthi  45276  expgrowth  45278  dvradcnv2  45290  binomcxplemradcnv  45295  binomcxplemdvbinom  45296  binomcxplemdvsum  45298  binomcxplemnotnn0  45299  binomcxp  45300  wessf1ornlem  46143  projf1o  46154  fsumsermpt  46535  fmuldfeqlem1  46538  fprodcn  46556  sumnnodd  46586  limsupvaluz  46662  limsupvaluz2  46692  supcnvlimsup  46694  supcnvlimsupmpt  46695  liminfval2  46722  liminflelimsuplem  46729  fprodsubrecnncnv  46862  fprodaddrecnncnv  46864  dvsinax  46867  fperdvper  46873  dvcosax  46880  ioodvbdlimc1lem1  46885  ioodvbdlimc1  46887  ioodvbdlimc2  46889  dvnmul  46897  dvnprodlem1  46900  dvnprodlem2  46901  dvnprodlem3  46902  dvnprod  46903  itgsin0pilem1  46904  itgiccshift  46934  stoweidlem2  46956  stoweidlem17  46971  stoweidlem32  46986  stoweidlem34  46988  stoweidlem43  46997  stirlinglem2  47029  stirlinglem3  47030  stirlinglem8  47035  dirkerval  47045  dirkerval2  47048  dirkeritg  47056  dirkercncflem3  47059  dirkercncf  47061  fourierdlem14  47075  fourierdlem18  47079  fourierdlem53  47113  fourierdlem62  47122  fourierdlem71  47131  fourierdlem74  47134  fourierdlem75  47135  fourierdlem76  47136  fourierdlem80  47140  fourierdlem81  47141  fourierdlem84  47144  fourierdlem88  47148  fourierdlem92  47152  fourierdlem93  47153  fourierdlem94  47154  fourierdlem95  47155  fourierdlem96  47156  fourierdlem97  47157  fourierdlem98  47158  fourierdlem99  47159  fourierdlem101  47161  fourierdlem103  47163  fourierdlem104  47164  fourierdlem105  47165  fourierdlem106  47166  fourierdlem107  47167  fourierdlem108  47168  fourierdlem110  47170  fourierdlem111  47171  fourierdlem112  47172  fourierdlem113  47173  fourierdlem115  47175  fouriersw  47185  elaa2  47188  etransclem1  47189  etransclem5  47193  etransclem6  47194  etransclem11  47199  etransclem13  47201  etransclem41  47229  etransclem47  47235  etransc  47237  ioorrnopn  47259  ioorrnopnxr  47261  subsaliuncl  47312  sge0resplit  47360  sge0fodjrnlem  47370  nnfoctbdj  47410  iundjiun  47414  voliunsge0lem  47426  meaiuninclem  47434  meaiuninc  47435  meaiininclem  47440  meaiininc  47441  omeiunltfirp  47473  carageniuncllem2  47476  carageniuncl  47477  0ome  47483  isomennd  47485  hoicvrrex  47510  ovn0  47520  ovnsubaddlem2  47525  ovnsubadd  47526  sge0hsphoire  47543  hoidmv1lelem3  47547  hoidmv1le  47548  hoidmvlelem1  47549  hoidmvlelem2  47550  hoidmvlelem3  47551  hoidmvlelem4  47552  hoidmvlelem5  47553  hoidmvle  47554  ovnhoilem2  47556  ovnhoi  47557  hspmbllem2  47581  hspmbl  47583  hoimbl  47585  opnvonmbllem2  47587  ovnsubadd2  47600  ovolval4  47605  ovolval5lem3  47608  ovnovollem3  47612  iccvonmbl  47633  vonioolem2  47635  vonioo  47636  vonicclem2  47638  vonicc  47639  smflimlem4  47728  smfsuplem2  47766  smflimsuplem1  47774  smflimsuplem8  47781  smflimsup  47782  fundcmpsurbijinjpreimafv  48433  prproropf1o  48533  isuspgrim0  48936  cycldlenngric  48970  isubgr3stgrlem8  49015  rmsupp0  49424  domnmsuppn0  49425  rmsuppss  49426  suppmptcfin  49432  ply1mulgsum  49446  lcoc0  49478  linc1  49481  lcoel0  49484  lcoss  49492  el0ldep  49522  lincresunit3  49537  isldepslvec2  49541  itcovalpclem2  49727  itcovalt2lem2  49732  veronesematrowd  50925  veronesematrowexpd  50926  veroquadgsumlem  50927  veroquadmodzerod  50928  amgmlemALT  50932