Theorem cbvmptv 5199

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 5200 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 2811	. . . 4 ⊢ (𝑥 = 𝑦 → (𝑥 ∈ 𝐴 ↔ 𝑦 ∈ 𝐴))
2		cbvmptv.1	. . . . 5 ⊢ (𝑥 = 𝑦 → 𝐵 = 𝐶)
3	2	eqeq2d 2740	. . . 4 ⊢ (𝑥 = 𝑦 → (𝑧 = 𝐵 ↔ 𝑧 = 𝐶))
4	1, 3	anbi12d 632	. . 3 ⊢ (𝑥 = 𝑦 → ((𝑥 ∈ 𝐴 ∧ 𝑧 = 𝐵) ↔ (𝑦 ∈ 𝐴 ∧ 𝑧 = 𝐶)))
5	4	cbvopab1v 5173	. 2 ⊢ {⟨𝑥, 𝑧⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑧 = 𝐵)} = {⟨𝑦, 𝑧⟩ ∣ (𝑦 ∈ 𝐴 ∧ 𝑧 = 𝐶)}
6		df-mpt 5177	. 2 ⊢ (𝑥 ∈ 𝐴 ↦ 𝐵) = {⟨𝑥, 𝑧⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑧 = 𝐵)}
7		df-mpt 5177	. 2 ⊢ (𝑦 ∈ 𝐴 ↦ 𝐶) = {⟨𝑦, 𝑧⟩ ∣ (𝑦 ∈ 𝐴 ∧ 𝑧 = 𝐶)}
8	5, 6, 7	3eqtr4i 2762	1 ⊢ (𝑥 ∈ 𝐴 ↦ 𝐵) = (𝑦 ∈ 𝐴 ↦ 𝐶)

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1540   ∈ wcel 2109  {copab 5157   ↦ cmpt 5176

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-rab 3397  df-v 3440  df-dif 3908  df-un 3910  df-ss 3922  df-nul 4287  df-if 4479  df-sn 4580  df-pr 4582  df-op 4586  df-opab 5158  df-mpt 5177

This theorem is referenced by:  fnmptfvd  6979  mptcnfimad  7928  onnseq  8274  rdgsucmpt2  8359  frsucmpt2  8369  fsetfocdm  8795  fsetprcnex  8796  resixpfo  8870  pw2f1olem  9005  xpmapen  9069  dffi3  9340  ordtypecbv  9428  inf3lema  9539  cantnflem1  9604  cnfcomlem  9614  infxpenc2  9935  fseqenlem1  9937  dfac8a  9943  dfac12r  10060  r1om  10156  fictb  10157  cfsmo  10184  coftr  10186  fin23lem38  10262  compsscnv  10284  isf34lem1  10285  compss  10289  fin1a2lem1  10313  fin1a2lem3  10315  fin1a2lem13  10325  itunisuc  10332  hsmex  10345  domtriom  10356  axdc2  10362  zorn2g  10416  ttukey2g  10429  axdc  10434  konigth  10482  pwcfsdom  10496  canthp1  10567  wunex2  10651  wuncval2  10660  negiso  12123  infrenegsup  12126  rpnnen1  12902  caurcvg2  15603  caucvg  15604  summo  15642  zsum  15643  fsum  15645  ackbijnn  15753  cbvprodv  15839  prodmo  15861  zprod  15862  fprod  15866  iprodmul  15928  bpolyval  15974  phimullem  16708  eulerth  16712  iserodd  16765  prmreclem5  16850  prmrec  16852  vdwlem7  16917  vdwlem9  16919  vdwlem10  16920  ramub1  16958  ramcl  16959  yonedalem4c  18201  yonedalem3b  18203  gsumwspan  18738  smndex1iidm  18793  smndex1gid  18795  smndex2dlinvh  18809  grplactcnv  18940  gicqusker  19185  galactghm  19301  symgfixfo  19336  pmtrdifwrdel  19382  pmtrdifwrdel2  19383  odf1o2  19470  sylow1lem2  19496  sylow1  19500  sylow2b  19520  sylow3lem1  19524  sylow3lem5  19528  sylow3  19530  efgtf  19619  efgsval  19628  ghmcyg  19793  cycsubgcyg  19798  ablfaclem3  19986  ablfac2  19988  srgbinomlem4  20132  funcrngcsetcALT  20544  fidomndrnglem  20675  isphld  21579  frlmphl  21706  mplmonmul  21959  evlslem2  22002  mat1ric  22390  mdetralt  22511  smadiadetlem3  22571  pmatcollpw3lem  22686  mp2pm2mplem5  22713  mp2pm2mp  22714  pm2mpmhmlem2  22722  cpmidpmat  22776  cpmadugsumlemF  22779  cpmadugsumfi  22780  cpmadumatpoly  22786  chcoeffeqlem  22788  cayleyhamilton0  22792  cayleyhamilton  22793  cayleyhamiltonALT  22794  cayleyhamilton1  22795  ordtbaslem  23091  ordtbas2  23094  lly1stc  23399  ptpjopn  23515  xkohmeo  23718  fbasrn  23787  elfm  23850  tmdmulg  23995  tmdgsum  23998  qustgpopn  24023  tsmsfbas  24031  tsmsf1o  24048  ustuqtoplem  24143  utopsnneip  24152  fmucnd  24195  ucnextcn  24207  met1stc  24425  prdsxmslem2  24433  metustto  24457  metustexhalf  24460  metuust  24464  cfilucfil2  24465  metuel  24468  metuel2  24469  psmetutop  24471  restmetu  24474  metucn  24475  xrge0tsms  24739  metdsge  24754  expcn  24779  expcnOLD  24781  pi1xfrcnv  24973  minveclem3b  25344  minveclem5  25349  minvec  25352  ovollb2  25406  ovolshftlem2  25427  ovolscalem2  25431  ovolicc  25440  ioombl1  25479  uniioombllem6  25505  volsup2  25522  vitali  25530  mbfi1fseq  25638  mbfmullem  25642  itg2seq  25659  itg2i1fseq  25672  itg2addlem  25675  itg2cnlem1  25678  itg2cn  25680  cbvitgv  25694  dvfsumrlimge0  25953  plyadd  26138  plymul  26139  coeeu  26146  coeid  26159  dvply2g  26208  dvply2gOLD  26209  plydivex  26221  elqaalem2  26244  elqaa  26246  taylthlem1  26297  taylth  26300  pserval  26335  radcnvlem2  26339  radcnvlt2  26344  dvradcnv  26346  pserulm  26347  psercn  26352  pserdvlem2  26354  pserdv  26355  efgh  26466  eff1olem  26473  circgrp  26477  circsubm  26478  logno1  26561  emcl  26929  harmonicbnd  26930  harmonicbnd2  26931  basel  27016  musum  27117  dchr1  27184  dchrptlem2  27192  dchrpt  27194  lgsqrlem4  27276  lgseisenlem3  27304  2sqlem1  27344  dchrmusumlema  27420  dchrmusum2  27421  dchrvmasumlema  27427  dchrvmasumiflem1  27428  dchrisum0ff  27434  dchrisum0lema  27441  dchrisum0lem1b  27442  dchrisum0lem2a  27444  nosupcbv  27630  noinfcbv  27645  precsexlemcbv  28131  seqsfn  28226  seqsp1  28228  wlknwwlksnbij  29851  clwlkclwwlken  29974  clwlknf1oclwwlkn  30046  frgrncvvdeqlem8  30268  frgrncvvdeqlem9  30269  numclwwlk1lem2  30322  ubthlem3  30834  minveco  30846  htth  30880  fsuppcurry1  32681  fsuppcurry2  32682  gsumhashmul  33027  xrge0tsmsd  33028  elrgspnlem1  33192  elrgspnlem2  33193  elrgspn  33196  elrgspnsubrunlem1  33197  elrgspnsubrunlem2  33198  elrgspnsubrun  33199  idomsubr  33258  nsgmgc  33359  nsgqusf1olem1  33360  lmicqusker  33365  ricqusker  33374  elrspunidl  33375  elrspunsn  33376  zringfrac  33501  ply1degltdim  33595  lbsdiflsp0  33598  fedgmullem1  33601  fedgmul  33603  assarrginv  33608  evls1fldgencl  33641  fldextrspunlsplem  33644  fldextrspunlsp  33645  algextdeglem4  33686  algextdeg  33691  constrcbvlem  33721  madjusmdetlem2  33794  madjusmdet  33797  zartop  33842  zartopon  33843  zart0  33845  zarmxt1  33846  zarcmp  33848  rhmpreimacn  33851  xrge0mulc1cn  33907  xrge0tmd  33911  xrge0tmdALT  33912  cbvesumv  34009  gsumesum  34025  esumlub  34026  esumpcvgval  34044  esumcvg  34052  esumcvg2  34053  eulerpartlems  34327  eulerpart  34349  fibp1  34368  rrvadd  34419  ballotlemfval  34457  ballotlemi  34468  ballotlemsval  34476  ballotlemsv  34477  ballotlemsf1o  34481  ballotlemrval  34485  ballotlemrinv  34501  signsply0  34518  actfunsnf1o  34571  actfunsnrndisj  34572  itgexpif  34573  hgt750lemb  34623  onvf1odlem3  35077  derangfmla  35162  erdsze  35174  pconnpi1  35209  cvmscbv  35230  cvmsss2  35246  cvmliftlem15  35270  cvmlift2  35288  cvmlift3  35300  elmrsubrn  35492  iprodefisum  35713  cbvprodvw2  36220  cbvitgvw2  36221  knoppcnlem7  36472  knoppf  36508  f1omptsn  37310  mptsnun  37312  fin2so  37586  poimirlem27  37626  broucube  37633  ftc1anclem5  37676  ftc1anclem6  37677  sdclem2  37721  prdstotbnd  37773  prdsbnd2  37774  heiborlem10  37799  lshpkrcl  39094  tendoplcbv  40754  tendo0cbv  40765  tendoicbv  40772  lcfl7N  41480  lcf1o  41530  hdmap1cbv  41781  frlmsnic  42513  evlselv  42560  mzpclval  42698  mzpcompact2lem  42724  rmxyval  42888  dnnumch1  43017  aomclem3  43029  aomclem8  43034  dfac21  43039  pwfi2f1o  43069  dftrcl3  43693  dfrtrcl3  43706  rfovcnvf1od  43977  fsovrfovd  43982  fsovcnvlem  43986  dssmapnvod  43993  clsk3nimkb  44013  radcnvrat  44287  expgrowthi  44306  expgrowth  44308  dvradcnv2  44320  binomcxplemradcnv  44325  binomcxplemdvbinom  44326  binomcxplemdvsum  44328  binomcxplemnotnn0  44329  binomcxp  44330  wessf1ornlem  45163  projf1o  45175  fsumsermpt  45561  fmuldfeqlem1  45564  fprodcn  45582  sumnnodd  45612  limsupvaluz  45690  limsupvaluz2  45720  supcnvlimsup  45722  supcnvlimsupmpt  45723  liminfval2  45750  liminflelimsuplem  45757  fprodsubrecnncnv  45890  fprodaddrecnncnv  45892  dvsinax  45895  fperdvper  45901  dvcosax  45908  ioodvbdlimc1lem1  45913  ioodvbdlimc1  45915  ioodvbdlimc2  45917  dvnmul  45925  dvnprodlem1  45928  dvnprodlem2  45929  dvnprodlem3  45930  dvnprod  45931  itgsin0pilem1  45932  itgiccshift  45962  stoweidlem2  45984  stoweidlem17  45999  stoweidlem32  46014  stoweidlem34  46016  stoweidlem43  46025  stirlinglem2  46057  stirlinglem3  46058  stirlinglem8  46063  dirkerval  46073  dirkerval2  46076  dirkeritg  46084  dirkercncflem3  46087  dirkercncf  46089  fourierdlem14  46103  fourierdlem18  46107  fourierdlem53  46141  fourierdlem62  46150  fourierdlem71  46159  fourierdlem74  46162  fourierdlem75  46163  fourierdlem76  46164  fourierdlem80  46168  fourierdlem81  46169  fourierdlem84  46172  fourierdlem88  46176  fourierdlem92  46180  fourierdlem93  46181  fourierdlem94  46182  fourierdlem95  46183  fourierdlem96  46184  fourierdlem97  46185  fourierdlem98  46186  fourierdlem99  46187  fourierdlem101  46189  fourierdlem103  46191  fourierdlem104  46192  fourierdlem105  46193  fourierdlem106  46194  fourierdlem107  46195  fourierdlem108  46196  fourierdlem110  46198  fourierdlem111  46199  fourierdlem112  46200  fourierdlem113  46201  fourierdlem115  46203  fouriersw  46213  elaa2  46216  etransclem1  46217  etransclem5  46221  etransclem6  46222  etransclem11  46227  etransclem13  46229  etransclem41  46257  etransclem47  46263  etransc  46265  ioorrnopn  46287  ioorrnopnxr  46289  subsaliuncl  46340  sge0resplit  46388  sge0fodjrnlem  46398  nnfoctbdj  46438  iundjiun  46442  voliunsge0lem  46454  meaiuninclem  46462  meaiuninc  46463  meaiininclem  46468  meaiininc  46469  omeiunltfirp  46501  carageniuncllem2  46504  carageniuncl  46505  0ome  46511  isomennd  46513  hoicvrrex  46538  ovn0  46548  ovnsubaddlem2  46553  ovnsubadd  46554  sge0hsphoire  46571  hoidmv1lelem3  46575  hoidmv1le  46576  hoidmvlelem1  46577  hoidmvlelem2  46578  hoidmvlelem3  46579  hoidmvlelem4  46580  hoidmvlelem5  46581  hoidmvle  46582  ovnhoilem2  46584  ovnhoi  46585  hspmbllem2  46609  hspmbl  46611  hoimbl  46613  opnvonmbllem2  46615  ovnsubadd2  46628  ovolval4  46633  ovolval5lem3  46636  ovnovollem3  46640  iccvonmbl  46661  vonioolem2  46663  vonioo  46664  vonicclem2  46666  vonicc  46667  smflimlem4  46756  smfsuplem2  46794  smflimsuplem1  46802  smflimsuplem8  46809  smflimsup  46810  fundcmpsurbijinjpreimafv  47392  prproropf1o  47492  isuspgrim0  47879  cycldlenngric  47913  isubgr3stgrlem8  47958  rmsupp0  48353  domnmsuppn0  48354  rmsuppss  48355  suppmptcfin  48361  ply1mulgsum  48376  lcoc0  48408  linc1  48411  lcoel0  48414  lcoss  48422  el0ldep  48452  lincresunit3  48467  isldepslvec2  48471  itcovalpclem2  48657  itcovalt2lem2  48662  amgmlemALT  49789