Theorem cbvmptv 5220

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 5221 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 2849	. . . 4 ⊢ (𝑥 = 𝑦 → (𝑥 ∈ 𝐴 ↔ 𝑦 ∈ 𝐴))
2		cbvmptv.1	. . . . 5 ⊢ (𝑥 = 𝑦 → 𝐵 = 𝐶)
3	2	eqeq2d 2777	. . . 4 ⊢ (𝑥 = 𝑦 → (𝑧 = 𝐵 ↔ 𝑧 = 𝐶))
4	1, 3	anbi12d 644	. . 3 ⊢ (𝑥 = 𝑦 → ((𝑥 ∈ 𝐴 ∧ 𝑧 = 𝐵) ↔ (𝑦 ∈ 𝐴 ∧ 𝑧 = 𝐶)))
5	4	cbvopab1v 5194	. 2 ⊢ {⟨𝑥, 𝑧⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑧 = 𝐵)} = {⟨𝑦, 𝑧⟩ ∣ (𝑦 ∈ 𝐴 ∧ 𝑧 = 𝐶)}
6		df-mpt 5198	. 2 ⊢ (𝑥 ∈ 𝐴 ↦ 𝐵) = {⟨𝑥, 𝑧⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑧 = 𝐵)}
7		df-mpt 5198	. 2 ⊢ (𝑦 ∈ 𝐴 ↦ 𝐶) = {⟨𝑦, 𝑧⟩ ∣ (𝑦 ∈ 𝐴 ∧ 𝑧 = 𝐶)}
8	5, 6, 7	3eqtr4i 2799	1 ⊢ (𝑥 ∈ 𝐴 ↦ 𝐵) = (𝑦 ∈ 𝐴 ↦ 𝐶)

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   = wceq 1570   ∈ wcel 2146  {copab 5178   ↦ cmpt 5197

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 2148  ax-9 2156  ax-ext 2738

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 2745  df-cleq 2758  df-clel 2841  df-rab 3420  df-v 3460  df-dif 3911  df-un 3913  df-ss 3925  df-nul 4290  df-if 4493  df-sn 4595  df-pr 4597  df-op 4601  df-opab 5179  df-mpt 5198

This theorem is used by:  fnmptfvd  7043  mptcnfimad  7992  onnseq  8340  rdgsucmpt2  8426  frsucmpt2  8436  fsetfocdm  8867  fsetprcnex  8868  resixpfo  8943  pw2f1olem  9079  xpmapen  9143  dffi3  9401  ordtypecbv  9489  inf3lema  9603  cantnflem1  9668  cnfcomlem  9678  infxpenc2  10025  fseqenlem1  10027  dfac8a  10033  dfac12r  10149  r1om  10245  fictb  10246  cfsmo  10273  coftr  10275  fin23lem38  10351  compsscnv  10373  isf34lem1  10374  compss  10378  fin1a2lem1  10402  fin1a2lem3  10404  fin1a2lem13  10414  itunisuc  10421  hsmex  10434  domtriom  10445  axdc2  10451  zorn2g  10505  ttukey2g  10518  axdc  10523  konigth  10572  pwcfsdom  10586  canthp1  10657  wunex2  10741  wuncval2  10750  negiso  12213  infrenegsup  12216  rpnnen1  13025  caurcvg2  15755  caucvg  15756  summo  15794  zsum  15795  fsum  15797  ackbijnn  15908  cbvprodv  15994  prodmo  16016  zprod  16017  fprod  16021  iprodmul  16083  bpolyval  16128  phimullem  16863  eulerth  16867  iserodd  16920  prmreclem5  17005  prmrec  17007  vdwlem7  17072  vdwlem9  17074  vdwlem10  17075  ramub1  17113  ramcl  17114  yonedalem4c  18358  yonedalem3b  18360  gsumwspan  18936  smndex1iidm  18991  smndex1gid  18994  smndex1gidOLD  18995  smndex2dlinvh  19010  grplactcnv  19140  gicqusker  19389  galactghm  19505  symgfixfo  19540  pmtrdifwrdel  19586  pmtrdifwrdel2  19587  odf1o2  19674  sylow1lem2  19700  sylow1  19704  sylow2b  19724  sylow3lem1  19728  sylow3lem5  19732  sylow3  19734  efgtf  19823  efgsval  19832  ghmcyg  19997  cycsubgcyg  20002  ablfaclem3  20190  ablfac2  20192  srgbinomlem4  20342  funcrngcsetcALT  20777  fidomndrnglem  20913  isphld  21841  frlmphl  21968  mplmonmul  22224  evlslem2  22267  mat1ric  22681  mdetralt  22802  smadiadetlem3  22862  pmatcollpw3lem  22977  mp2pm2mplem5  23004  mp2pm2mp  23005  pm2mpmhmlem2  23013  cpmidpmat  23067  cpmadugsumlemF  23070  cpmadugsumfi  23071  cpmadumatpoly  23077  chcoeffeqlem  23079  cayleyhamilton0  23083  cayleyhamilton  23084  cayleyhamiltonALT  23085  cayleyhamilton1  23086  ordtbaslem  23382  ordtbas2  23385  lly1stc  23690  ptpjopn  23806  xkohmeo  24009  fbasrn  24078  elfm  24141  tmdmulg  24286  tmdgsum  24289  qustgpopn  24314  tsmsfbas  24322  tsmsf1o  24339  ustuqtoplem  24433  utopsnneip  24442  fmucnd  24485  ucnextcn  24497  met1stc  24715  prdsxmslem2  24723  metustto  24747  metustexhalf  24750  metuust  24754  cfilucfil2  24755  metuel  24758  metuel2  24759  psmetutop  24761  restmetu  24764  metucn  24765  xrge0tsms  25029  metdsge  25044  expcn  25068  pi1xfrcnv  25253  minveclem3b  25624  minveclem5  25629  minvec  25632  ovollb2  25685  ovolshftlem2  25706  ovolscalem2  25710  ovolicc  25719  ioombl1  25758  uniioombllem6  25784  volsup2  25801  vitali  25809  mbfi1fseq  25917  mbfmullem  25921  itg2seq  25938  itg2i1fseq  25951  itg2addlem  25954  itg2cnlem1  25957  itg2cn  25959  cbvitgv  25973  dvfsumrlimge0  26226  plyadd  26411  plymul  26412  coeeu  26419  coeid  26432  dvply2g  26483  plydivex  26495  elqaalem2  26518  elqaa  26520  taylthlem1  26573  taylth  26575  pserval  26610  radcnvlem2  26614  radcnvlt2  26619  dvradcnv  26621  pserulm  26622  psercn  26626  pserdvlem2  26628  pserdv  26629  efgh  26743  eff1olem  26750  circgrp  26754  circsubm  26755  logno1  26838  emcl  27204  harmonicbnd  27205  harmonicbnd2  27206  basel  27291  musum  27392  dchr1  27458  dchrptlem2  27466  dchrpt  27468  lgsqrlem4  27550  lgseisenlem3  27578  2sqlem1  27618  dchrmusumlema  27694  dchrmusum2  27695  dchrvmasumlema  27701  dchrvmasumiflem1  27702  dchrisum0ff  27708  dchrisum0lema  27715  dchrisum0lem1b  27716  dchrisum0lem2a  27718  nosupcbv  27903  noinfcbv  27918  precsexlemcbv  28436  seqsfn  28539  seqsp1  28541  wlknwwlksnbij  30274  clwlkclwwlken  30400  clwlknf1oclwwlkn  30472  frgrncvvdeqlem8  30694  frgrncvvdeqlem9  30695  numclwwlk1lem2  30748  ubthlem3  31261  minveco  31273  htth  31307  fsuppcurry1  33106  fsuppcurry2  33107  gsumhashmul  33418  gsummulsubdishift1  33419  gsummulsubdishift1s  33421  gsummulsubdishift2s  33422  xrge0tsmsd  33424  elrgspnlem1  33593  elrgspnlem2  33594  elrgspn  33597  elrgspnsubrunlem1  33598  elrgspnsubrunlem2  33599  elrgspnsubrun  33600  idomsubr  33661  nsgmgc  33752  nsgqusf1olem1  33753  lmicqusker  33758  ricqusker  33766  elrspunidl  33767  elrspunsn  33768  zringfrac  33875  0mplric  33936  selvply1rhmlemb  33940  selvply1rhmlem3  33943  selvply1rhmlem5  33945  selvply1rhm  33946  mplidom  33949  mplvrpmga  33966  mplvrpmrhm  33968  psrgsum  33969  psrmonmul  33971  psrmonprod  33973  splysubrg  33981  issply  33982  esplyfvaln  33995  vietalem  34000  vieta  34001  ply1degltdim  34044  lbsdiflsp0  34047  fedgmullem1  34050  fedgmul  34052  assarrginv  34057  evls1fldgencl  34091  fldextrspunlsplem  34094  fldextrspunlsp  34095  extdgfialglem2  34114  extdgfialg  34115  algextdeglem4  34141  algextdeg  34146  constrcbvlem  34176  madjusmdetlem2  34249  madjusmdet  34252  zartop  34297  zartopon  34298  zart0  34300  zarmxt1  34301  zarcmp  34303  rhmpreimacn  34306  xrge0mulc1cn  34362  xrge0tmd  34366  xrge0tmdALT  34367  cbvesumv  34464  gsumesum  34480  esumlub  34481  esumpcvgval  34499  esumcvg  34507  esumcvg2  34508  eulerpartlems  34782  eulerpart  34804  fibp1  34823  rrvadd  34874  ballotlemfval  34912  ballotlemi  34923  ballotlemsval  34931  ballotlemsv  34932  ballotlemsf1o  34936  ballotlemrval  34940  ballotlemrinv  34956  signsply0  34970  actfunsnf1o  35023  actfunsnrndisj  35024  itgexpif  35025  hgt750lemb  35075  onvf1odlem3  35613  derangfmla  35703  erdsze  35715  pconnpi1  35750  cvmscbv  35771  cvmsss2  35787  cvmliftlem15  35811  cvmlift2  35829  cvmlift3  35841  elmrsubrn  36033  iprodefisum  36254  cbvprodvw2  36800  cbvitgvw2  36801  knoppcnlem7  37129  knoppf  37165  f1omptsn  38024  mptsnun  38026  fin2so  38299  poimirlem27  38339  broucube  38346  ftc1anclem5  38389  ftc1anclem6  38390  sdclem2  38434  prdstotbnd  38486  prdsbnd2  38487  heiborlem10  38512  lshpkrcl  39931  tendoplcbv  41590  tendo0cbv  41601  tendoicbv  41608  lcfl7N  42316  lcf1o  42366  hdmap1cbv  42617  frlmsnic  43349  evlselv  43362  mzpclval  43497  mzpcompact2lem  43523  rmxyval  43683  dnnumch1  43812  aomclem3  43824  aomclem8  43829  dfac21  43834  pwfi2f1o  43864  dftrcl3  44487  dfrtrcl3  44500  rfovcnvf1od  44771  fsovrfovd  44776  fsovcnvlem  44780  dssmapnvod  44787  clsk3nimkb  44807  radcnvrat  45065  expgrowthi  45084  expgrowth  45086  dvradcnv2  45098  binomcxplemradcnv  45103  binomcxplemdvbinom  45104  binomcxplemdvsum  45106  binomcxplemnotnn0  45107  binomcxp  45108  wessf1ornlem  45944  projf1o  45955  fsumsermpt  46336  fmuldfeqlem1  46339  fprodcn  46357  sumnnodd  46387  limsupvaluz  46463  limsupvaluz2  46493  supcnvlimsup  46495  supcnvlimsupmpt  46496  liminfval2  46523  liminflelimsuplem  46530  fprodsubrecnncnv  46663  fprodaddrecnncnv  46665  dvsinax  46668  fperdvper  46674  dvcosax  46681  ioodvbdlimc1lem1  46686  ioodvbdlimc1  46688  ioodvbdlimc2  46690  dvnmul  46698  dvnprodlem1  46701  dvnprodlem2  46702  dvnprodlem3  46703  dvnprod  46704  itgsin0pilem1  46705  itgiccshift  46735  stoweidlem2  46757  stoweidlem17  46772  stoweidlem32  46787  stoweidlem34  46789  stoweidlem43  46798  stirlinglem2  46830  stirlinglem3  46831  stirlinglem8  46836  dirkerval  46846  dirkerval2  46849  dirkeritg  46857  dirkercncflem3  46860  dirkercncf  46862  fourierdlem14  46876  fourierdlem18  46880  fourierdlem53  46914  fourierdlem62  46923  fourierdlem71  46932  fourierdlem74  46935  fourierdlem75  46936  fourierdlem76  46937  fourierdlem80  46941  fourierdlem81  46942  fourierdlem84  46945  fourierdlem88  46949  fourierdlem92  46953  fourierdlem93  46954  fourierdlem94  46955  fourierdlem95  46956  fourierdlem96  46957  fourierdlem97  46958  fourierdlem98  46959  fourierdlem99  46960  fourierdlem101  46962  fourierdlem103  46964  fourierdlem104  46965  fourierdlem105  46966  fourierdlem106  46967  fourierdlem107  46968  fourierdlem108  46969  fourierdlem110  46971  fourierdlem111  46972  fourierdlem112  46973  fourierdlem113  46974  fourierdlem115  46976  fouriersw  46986  elaa2  46989  etransclem1  46990  etransclem5  46994  etransclem6  46995  etransclem11  47000  etransclem13  47002  etransclem41  47030  etransclem47  47036  etransc  47038  ioorrnopn  47060  ioorrnopnxr  47062  subsaliuncl  47113  sge0resplit  47161  sge0fodjrnlem  47171  nnfoctbdj  47211  iundjiun  47215  voliunsge0lem  47227  meaiuninclem  47235  meaiuninc  47236  meaiininclem  47241  meaiininc  47242  omeiunltfirp  47274  carageniuncllem2  47277  carageniuncl  47278  0ome  47284  isomennd  47286  hoicvrrex  47311  ovn0  47321  ovnsubaddlem2  47326  ovnsubadd  47327  sge0hsphoire  47344  hoidmv1lelem3  47348  hoidmv1le  47349  hoidmvlelem1  47350  hoidmvlelem2  47351  hoidmvlelem3  47352  hoidmvlelem4  47353  hoidmvlelem5  47354  hoidmvle  47355  ovnhoilem2  47357  ovnhoi  47358  hspmbllem2  47382  hspmbl  47384  hoimbl  47386  opnvonmbllem2  47388  ovnsubadd2  47401  ovolval4  47406  ovolval5lem3  47409  ovnovollem3  47413  iccvonmbl  47434  vonioolem2  47436  vonioo  47437  vonicclem2  47439  vonicc  47440  smflimlem4  47529  smfsuplem2  47567  smflimsuplem1  47575  smflimsuplem8  47582  smflimsup  47583  fundcmpsurbijinjpreimafv  48197  prproropf1o  48297  isuspgrim0  48700  cycldlenngric  48734  isubgr3stgrlem8  48779  rmsupp0  49189  domnmsuppn0  49190  rmsuppss  49191  suppmptcfin  49197  ply1mulgsum  49211  lcoc0  49243  linc1  49246  lcoel0  49249  lcoss  49257  el0ldep  49287  lincresunit3  49302  isldepslvec2  49306  itcovalpclem2  49492  itcovalt2lem2  49497  amgmlemALT  50692