Theorem cbvmptv 5183

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 5184 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 2823	. . . 4 ⊢ (𝑥 = 𝑦 → (𝑥 ∈ 𝐴 ↔ 𝑦 ∈ 𝐴))
2		cbvmptv.1	. . . . 5 ⊢ (𝑥 = 𝑦 → 𝐵 = 𝐶)
3	2	eqeq2d 2751	. . . 4 ⊢ (𝑥 = 𝑦 → (𝑧 = 𝐵 ↔ 𝑧 = 𝐶))
4	1, 3	anbi12d 638	. . 3 ⊢ (𝑥 = 𝑦 → ((𝑥 ∈ 𝐴 ∧ 𝑧 = 𝐵) ↔ (𝑦 ∈ 𝐴 ∧ 𝑧 = 𝐶)))
5	4	cbvopab1v 5157	. 2 ⊢ {⟨𝑥, 𝑧⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑧 = 𝐵)} = {⟨𝑦, 𝑧⟩ ∣ (𝑦 ∈ 𝐴 ∧ 𝑧 = 𝐶)}
6		df-mpt 5161	. 2 ⊢ (𝑥 ∈ 𝐴 ↦ 𝐵) = {⟨𝑥, 𝑧⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑧 = 𝐵)}
7		df-mpt 5161	. 2 ⊢ (𝑦 ∈ 𝐴 ↦ 𝐶) = {⟨𝑦, 𝑧⟩ ∣ (𝑦 ∈ 𝐴 ∧ 𝑧 = 𝐶)}
8	5, 6, 7	3eqtr4i 2773	1 ⊢ (𝑥 ∈ 𝐴 ↦ 𝐵) = (𝑦 ∈ 𝐴 ↦ 𝐶)

Syntax hints:   → wi 4   ∧ wa 396   = wceq 1547   ∈ wcel 2119  {copab 5141   ↦ cmpt 5160

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2712

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-3an 1094  df-tru 1550  df-fal 1560  df-ex 1787  df-sb 2074  df-clab 2719  df-cleq 2732  df-clel 2815  df-rab 3393  df-v 3434  df-dif 3893  df-un 3895  df-ss 3907  df-nul 4269  df-if 4462  df-sn 4563  df-pr 4565  df-op 4569  df-opab 5142  df-mpt 5161

This theorem is referenced by:  fnmptfvd  6989  mptcnfimad  7935  onnseq  8281  rdgsucmpt2  8366  frsucmpt2  8376  fsetfocdm  8805  fsetprcnex  8806  resixpfo  8881  pw2f1olem  9016  xpmapen  9080  dffi3  9341  ordtypecbv  9429  inf3lema  9543  cantnflem1  9608  cnfcomlem  9618  infxpenc2  9942  fseqenlem1  9944  dfac8a  9950  dfac12r  10067  r1om  10163  fictb  10164  cfsmo  10191  coftr  10193  fin23lem38  10269  compsscnv  10291  isf34lem1  10292  compss  10296  fin1a2lem1  10320  fin1a2lem3  10322  fin1a2lem13  10332  itunisuc  10339  hsmex  10352  domtriom  10363  axdc2  10369  zorn2g  10423  ttukey2g  10436  axdc  10441  konigth  10490  pwcfsdom  10504  canthp1  10575  wunex2  10659  wuncval2  10668  negiso  12134  infrenegsup  12137  rpnnen1  12931  caurcvg2  15638  caucvg  15639  summo  15677  zsum  15678  fsum  15680  ackbijnn  15791  cbvprodv  15877  prodmo  15899  zprod  15900  fprod  15904  iprodmul  15966  bpolyval  16012  phimullem  16747  eulerth  16751  iserodd  16804  prmreclem5  16889  prmrec  16891  vdwlem7  16956  vdwlem9  16958  vdwlem10  16959  ramub1  16997  ramcl  16998  yonedalem4c  18241  yonedalem3b  18243  gsumwspan  18812  smndex1iidm  18867  smndex1gid  18870  smndex1gidOLD  18871  smndex2dlinvh  18886  grplactcnv  19017  gicqusker  19261  galactghm  19377  symgfixfo  19412  pmtrdifwrdel  19458  pmtrdifwrdel2  19459  odf1o2  19546  sylow1lem2  19572  sylow1  19576  sylow2b  19596  sylow3lem1  19600  sylow3lem5  19604  sylow3  19606  efgtf  19695  efgsval  19704  ghmcyg  19869  cycsubgcyg  19874  ablfaclem3  20062  ablfac2  20064  srgbinomlem4  20208  funcrngcsetcALT  20620  fidomndrnglem  20751  isphld  21636  frlmphl  21763  mplmonmul  22019  evlslem2  22062  mat1ric  22477  mdetralt  22598  smadiadetlem3  22658  pmatcollpw3lem  22773  mp2pm2mplem5  22800  mp2pm2mp  22801  pm2mpmhmlem2  22809  cpmidpmat  22863  cpmadugsumlemF  22866  cpmadugsumfi  22867  cpmadumatpoly  22873  chcoeffeqlem  22875  cayleyhamilton0  22879  cayleyhamilton  22880  cayleyhamiltonALT  22881  cayleyhamilton1  22882  ordtbaslem  23178  ordtbas2  23181  lly1stc  23486  ptpjopn  23602  xkohmeo  23805  fbasrn  23874  elfm  23937  tmdmulg  24082  tmdgsum  24085  qustgpopn  24110  tsmsfbas  24118  tsmsf1o  24135  ustuqtoplem  24229  utopsnneip  24238  fmucnd  24281  ucnextcn  24293  met1stc  24511  prdsxmslem2  24519  metustto  24543  metustexhalf  24546  metuust  24550  cfilucfil2  24551  metuel  24554  metuel2  24555  psmetutop  24557  restmetu  24560  metucn  24561  xrge0tsms  24825  metdsge  24840  expcn  24864  pi1xfrcnv  25049  minveclem3b  25420  minveclem5  25425  minvec  25428  ovollb2  25481  ovolshftlem2  25502  ovolscalem2  25506  ovolicc  25515  ioombl1  25554  uniioombllem6  25580  volsup2  25597  vitali  25605  mbfi1fseq  25713  mbfmullem  25717  itg2seq  25734  itg2i1fseq  25747  itg2addlem  25750  itg2cnlem1  25753  itg2cn  25755  cbvitgv  25769  dvfsumrlimge0  26022  plyadd  26207  plymul  26208  coeeu  26215  coeid  26228  dvply2g  26276  plydivex  26288  elqaalem2  26311  elqaa  26313  taylthlem1  26363  taylth  26365  pserval  26400  radcnvlem2  26404  radcnvlt2  26409  dvradcnv  26411  pserulm  26412  psercn  26416  pserdvlem2  26418  pserdv  26419  efgh  26530  eff1olem  26537  circgrp  26541  circsubm  26542  logno1  26625  emcl  26991  harmonicbnd  26992  harmonicbnd2  26993  basel  27078  musum  27179  dchr1  27245  dchrptlem2  27253  dchrpt  27255  lgsqrlem4  27337  lgseisenlem3  27365  2sqlem1  27405  dchrmusumlema  27481  dchrmusum2  27482  dchrvmasumlema  27488  dchrvmasumiflem1  27489  dchrisum0ff  27495  dchrisum0lema  27502  dchrisum0lem1b  27503  dchrisum0lem2a  27505  nosupcbv  27691  noinfcbv  27706  precsexlemcbv  28223  seqsfn  28326  seqsp1  28328  wlknwwlksnbij  29981  clwlkclwwlken  30107  clwlknf1oclwwlkn  30179  frgrncvvdeqlem8  30401  frgrncvvdeqlem9  30402  numclwwlk1lem2  30455  ubthlem3  30968  minveco  30980  htth  31014  fsuppcurry1  32823  fsuppcurry2  32824  gsumhashmul  33155  gsummulsubdishift1  33156  gsummulsubdishift1s  33158  gsummulsubdishift2s  33159  xrge0tsmsd  33161  elrgspnlem1  33330  elrgspnlem2  33331  elrgspn  33334  elrgspnsubrunlem1  33335  elrgspnsubrunlem2  33336  elrgspnsubrun  33337  idomsubr  33400  nsgmgc  33502  nsgqusf1olem1  33503  lmicqusker  33508  ricqusker  33517  elrspunidl  33518  elrspunsn  33519  zringfrac  33644  0mplric  33706  selvply1rhmlemb  33710  selvply1rhmlem3  33713  selvply1rhmlem5  33715  selvply1rhm  33716  mplidom  33719  mplvrpmga  33736  mplvrpmrhm  33738  psrgsum  33739  psrmonmul  33741  psrmonprod  33743  splysubrg  33751  issply  33752  esplyfvaln  33765  vietalem  33770  vieta  33771  ply1degltdim  33814  lbsdiflsp0  33817  fedgmullem1  33820  fedgmul  33822  assarrginv  33827  evls1fldgencl  33861  fldextrspunlsplem  33864  fldextrspunlsp  33865  extdgfialglem2  33884  extdgfialg  33885  algextdeglem4  33911  algextdeg  33916  constrcbvlem  33946  madjusmdetlem2  34019  madjusmdet  34022  zartop  34067  zartopon  34068  zart0  34070  zarmxt1  34071  zarcmp  34073  rhmpreimacn  34076  xrge0mulc1cn  34132  xrge0tmd  34136  xrge0tmdALT  34137  cbvesumv  34234  gsumesum  34250  esumlub  34251  esumpcvgval  34269  esumcvg  34277  esumcvg2  34278  eulerpartlems  34551  eulerpart  34573  fibp1  34592  rrvadd  34643  ballotlemfval  34681  ballotlemi  34692  ballotlemsval  34700  ballotlemsv  34701  ballotlemsf1o  34705  ballotlemrval  34709  ballotlemrinv  34725  signsply0  34742  actfunsnf1o  34795  actfunsnrndisj  34796  itgexpif  34797  hgt750lemb  34847  onvf1odlem3  35340  derangfmla  35425  erdsze  35437  pconnpi1  35472  cvmscbv  35493  cvmsss2  35509  cvmliftlem15  35533  cvmlift2  35551  cvmlift3  35563  elmrsubrn  35755  iprodefisum  35976  cbvprodvw2  36482  cbvitgvw2  36483  knoppcnlem7  36812  knoppf  36848  f1omptsn  37706  mptsnun  37708  fin2so  37981  poimirlem27  38021  broucube  38028  ftc1anclem5  38071  ftc1anclem6  38072  sdclem2  38116  prdstotbnd  38168  prdsbnd2  38169  heiborlem10  38194  lshpkrcl  39615  tendoplcbv  41274  tendo0cbv  41285  tendoicbv  41292  lcfl7N  42000  lcf1o  42050  hdmap1cbv  42301  frlmsnic  43033  evlselv  43046  mzpclval  43181  mzpcompact2lem  43207  rmxyval  43367  dnnumch1  43496  aomclem3  43508  aomclem8  43513  dfac21  43518  pwfi2f1o  43548  dftrcl3  44171  dfrtrcl3  44184  rfovcnvf1od  44455  fsovrfovd  44460  fsovcnvlem  44464  dssmapnvod  44471  clsk3nimkb  44491  radcnvrat  44765  expgrowthi  44784  expgrowth  44786  dvradcnv2  44798  binomcxplemradcnv  44803  binomcxplemdvbinom  44804  binomcxplemdvsum  44806  binomcxplemnotnn0  44807  binomcxp  44808  wessf1ornlem  45639  projf1o  45650  fsumsermpt  46031  fmuldfeqlem1  46034  fprodcn  46052  sumnnodd  46082  limsupvaluz  46158  limsupvaluz2  46188  supcnvlimsup  46190  supcnvlimsupmpt  46191  liminfval2  46218  liminflelimsuplem  46225  fprodsubrecnncnv  46358  fprodaddrecnncnv  46360  dvsinax  46363  fperdvper  46369  dvcosax  46376  ioodvbdlimc1lem1  46381  ioodvbdlimc1  46383  ioodvbdlimc2  46385  dvnmul  46393  dvnprodlem1  46396  dvnprodlem2  46397  dvnprodlem3  46398  dvnprod  46399  itgsin0pilem1  46400  itgiccshift  46430  stoweidlem2  46452  stoweidlem17  46467  stoweidlem32  46482  stoweidlem34  46484  stoweidlem43  46493  stirlinglem2  46525  stirlinglem3  46526  stirlinglem8  46531  dirkerval  46541  dirkerval2  46544  dirkeritg  46552  dirkercncflem3  46555  dirkercncf  46557  fourierdlem14  46571  fourierdlem18  46575  fourierdlem53  46609  fourierdlem62  46618  fourierdlem71  46627  fourierdlem74  46630  fourierdlem75  46631  fourierdlem76  46632  fourierdlem80  46636  fourierdlem81  46637  fourierdlem84  46640  fourierdlem88  46644  fourierdlem92  46648  fourierdlem93  46649  fourierdlem94  46650  fourierdlem95  46651  fourierdlem96  46652  fourierdlem97  46653  fourierdlem98  46654  fourierdlem99  46655  fourierdlem101  46657  fourierdlem103  46659  fourierdlem104  46660  fourierdlem105  46661  fourierdlem106  46662  fourierdlem107  46663  fourierdlem108  46664  fourierdlem110  46666  fourierdlem111  46667  fourierdlem112  46668  fourierdlem113  46669  fourierdlem115  46671  fouriersw  46681  elaa2  46684  etransclem1  46685  etransclem5  46689  etransclem6  46690  etransclem11  46695  etransclem13  46697  etransclem41  46725  etransclem47  46731  etransc  46733  ioorrnopn  46755  ioorrnopnxr  46757  subsaliuncl  46808  sge0resplit  46856  sge0fodjrnlem  46866  nnfoctbdj  46906  iundjiun  46910  voliunsge0lem  46922  meaiuninclem  46930  meaiuninc  46931  meaiininclem  46936  meaiininc  46937  omeiunltfirp  46969  carageniuncllem2  46972  carageniuncl  46973  0ome  46979  isomennd  46981  hoicvrrex  47006  ovn0  47016  ovnsubaddlem2  47021  ovnsubadd  47022  sge0hsphoire  47039  hoidmv1lelem3  47043  hoidmv1le  47044  hoidmvlelem1  47045  hoidmvlelem2  47046  hoidmvlelem3  47047  hoidmvlelem4  47048  hoidmvlelem5  47049  hoidmvle  47050  ovnhoilem2  47052  ovnhoi  47053  hspmbllem2  47077  hspmbl  47079  hoimbl  47081  opnvonmbllem2  47083  ovnsubadd2  47096  ovolval4  47101  ovolval5lem3  47104  ovnovollem3  47108  iccvonmbl  47129  vonioolem2  47131  vonioo  47132  vonicclem2  47134  vonicc  47135  smflimlem4  47224  smfsuplem2  47262  smflimsuplem1  47270  smflimsuplem8  47277  smflimsup  47278  fundcmpsurbijinjpreimafv  47889  prproropf1o  47989  isuspgrim0  48392  cycldlenngric  48426  isubgr3stgrlem8  48471  rmsupp0  48866  domnmsuppn0  48867  rmsuppss  48868  suppmptcfin  48874  ply1mulgsum  48888  lcoc0  48920  linc1  48923  lcoel0  48926  lcoss  48934  el0ldep  48964  lincresunit3  48979  isldepslvec2  48983  itcovalpclem2  49169  itcovalt2lem2  49174  amgmlemALT  50300