Theorem cbvmptv 5216

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 5217 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 2846	. . . 4 ⊢ (𝑥 = 𝑦 → (𝑥 ∈ 𝐴 ↔ 𝑦 ∈ 𝐴))
2		cbvmptv.1	. . . . 5 ⊢ (𝑥 = 𝑦 → 𝐵 = 𝐶)
3	2	eqeq2d 2774	. . . 4 ⊢ (𝑥 = 𝑦 → (𝑧 = 𝐵 ↔ 𝑧 = 𝐶))
4	1, 3	anbi12d 643	. . 3 ⊢ (𝑥 = 𝑦 → ((𝑥 ∈ 𝐴 ∧ 𝑧 = 𝐵) ↔ (𝑦 ∈ 𝐴 ∧ 𝑧 = 𝐶)))
5	4	cbvopab1v 5190	. 2 ⊢ {⟨𝑥, 𝑧⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑧 = 𝐵)} = {⟨𝑦, 𝑧⟩ ∣ (𝑦 ∈ 𝐴 ∧ 𝑧 = 𝐶)}
6		df-mpt 5194	. 2 ⊢ (𝑥 ∈ 𝐴 ↦ 𝐵) = {⟨𝑥, 𝑧⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑧 = 𝐵)}
7		df-mpt 5194	. 2 ⊢ (𝑦 ∈ 𝐴 ↦ 𝐶) = {⟨𝑦, 𝑧⟩ ∣ (𝑦 ∈ 𝐴 ∧ 𝑧 = 𝐶)}
8	5, 6, 7	3eqtr4i 2796	1 ⊢ (𝑥 ∈ 𝐴 ↦ 𝐵) = (𝑦 ∈ 𝐴 ↦ 𝐶)

Syntax hints:   → wi 4   ∧ wa 400   = wceq 1570   ∈ wcel 2143  {copab 5174   ↦ cmpt 5193

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-rab 3417  df-v 3457  df-dif 3909  df-un 3911  df-ss 3923  df-nul 4288  df-if 4489  df-sn 4591  df-pr 4593  df-op 4597  df-opab 5175  df-mpt 5194

This theorem is referenced by:  fnmptfvd  7038  mptcnfimad  7984  onnseq  8332  rdgsucmpt2  8418  frsucmpt2  8428  fsetfocdm  8859  fsetprcnex  8860  resixpfo  8935  pw2f1olem  9070  xpmapen  9134  dffi3  9392  ordtypecbv  9480  inf3lema  9594  cantnflem1  9659  cnfcomlem  9669  infxpenc2  10007  fseqenlem1  10009  dfac8a  10015  dfac12r  10131  r1om  10227  fictb  10228  cfsmo  10256  coftr  10258  fin23lem38  10334  compsscnv  10356  isf34lem1  10357  compss  10361  fin1a2lem1  10385  fin1a2lem3  10387  fin1a2lem13  10397  itunisuc  10404  hsmex  10417  domtriom  10428  axdc2  10434  zorn2g  10488  ttukey2g  10501  axdc  10506  konigth  10555  pwcfsdom  10569  canthp1  10640  wunex2  10724  wuncval2  10733  negiso  12196  infrenegsup  12199  rpnnen1  13008  caurcvg2  15731  caucvg  15732  summo  15770  zsum  15771  fsum  15773  ackbijnn  15884  cbvprodv  15970  prodmo  15992  zprod  15993  fprod  15997  iprodmul  16059  bpolyval  16104  phimullem  16839  eulerth  16843  iserodd  16896  prmreclem5  16981  prmrec  16983  vdwlem7  17048  vdwlem9  17050  vdwlem10  17051  ramub1  17089  ramcl  17090  yonedalem4c  18334  yonedalem3b  18336  gsumwspan  18906  smndex1iidm  18961  smndex1gid  18964  smndex1gidOLD  18965  smndex2dlinvh  18980  grplactcnv  19110  gicqusker  19359  galactghm  19475  symgfixfo  19510  pmtrdifwrdel  19556  pmtrdifwrdel2  19557  odf1o2  19644  sylow1lem2  19670  sylow1  19674  sylow2b  19694  sylow3lem1  19698  sylow3lem5  19702  sylow3  19704  efgtf  19793  efgsval  19802  ghmcyg  19967  cycsubgcyg  19972  ablfaclem3  20160  ablfac2  20162  srgbinomlem4  20312  funcrngcsetcALT  20727  fidomndrnglem  20857  isphld  21785  frlmphl  21912  mplmonmul  22168  evlslem2  22211  mat1ric  22625  mdetralt  22746  smadiadetlem3  22806  pmatcollpw3lem  22921  mp2pm2mplem5  22948  mp2pm2mp  22949  pm2mpmhmlem2  22957  cpmidpmat  23011  cpmadugsumlemF  23014  cpmadugsumfi  23015  cpmadumatpoly  23021  chcoeffeqlem  23023  cayleyhamilton0  23027  cayleyhamilton  23028  cayleyhamiltonALT  23029  cayleyhamilton1  23030  ordtbaslem  23326  ordtbas2  23329  lly1stc  23634  ptpjopn  23750  xkohmeo  23953  fbasrn  24022  elfm  24085  tmdmulg  24230  tmdgsum  24233  qustgpopn  24258  tsmsfbas  24266  tsmsf1o  24283  ustuqtoplem  24377  utopsnneip  24386  fmucnd  24429  ucnextcn  24441  met1stc  24659  prdsxmslem2  24667  metustto  24691  metustexhalf  24694  metuust  24698  cfilucfil2  24699  metuel  24702  metuel2  24703  psmetutop  24705  restmetu  24708  metucn  24709  xrge0tsms  24973  metdsge  24988  expcn  25012  pi1xfrcnv  25197  minveclem3b  25568  minveclem5  25573  minvec  25576  ovollb2  25629  ovolshftlem2  25650  ovolscalem2  25654  ovolicc  25663  ioombl1  25702  uniioombllem6  25728  volsup2  25745  vitali  25753  mbfi1fseq  25861  mbfmullem  25865  itg2seq  25882  itg2i1fseq  25895  itg2addlem  25898  itg2cnlem1  25901  itg2cn  25903  cbvitgv  25917  dvfsumrlimge0  26170  plyadd  26355  plymul  26356  coeeu  26363  coeid  26376  dvply2g  26427  plydivex  26439  elqaalem2  26462  elqaa  26464  taylthlem1  26517  taylth  26519  pserval  26554  radcnvlem2  26558  radcnvlt2  26563  dvradcnv  26565  pserulm  26566  psercn  26570  pserdvlem2  26572  pserdv  26573  efgh  26687  eff1olem  26694  circgrp  26698  circsubm  26699  logno1  26782  emcl  27148  harmonicbnd  27149  harmonicbnd2  27150  basel  27235  musum  27336  dchr1  27402  dchrptlem2  27410  dchrpt  27412  lgsqrlem4  27494  lgseisenlem3  27522  2sqlem1  27562  dchrmusumlema  27638  dchrmusum2  27639  dchrvmasumlema  27645  dchrvmasumiflem1  27646  dchrisum0ff  27652  dchrisum0lema  27659  dchrisum0lem1b  27660  dchrisum0lem2a  27662  nosupcbv  27847  noinfcbv  27862  precsexlemcbv  28380  seqsfn  28483  seqsp1  28485  wlknwwlksnbij  30218  clwlkclwwlken  30344  clwlknf1oclwwlkn  30416  frgrncvvdeqlem8  30638  frgrncvvdeqlem9  30639  numclwwlk1lem2  30692  ubthlem3  31205  minveco  31217  htth  31251  fsuppcurry1  33050  fsuppcurry2  33051  gsumhashmul  33368  gsummulsubdishift1  33369  gsummulsubdishift1s  33371  gsummulsubdishift2s  33372  xrge0tsmsd  33374  elrgspnlem1  33543  elrgspnlem2  33544  elrgspn  33547  elrgspnsubrunlem1  33548  elrgspnsubrunlem2  33549  elrgspnsubrun  33550  idomsubr  33611  nsgmgc  33702  nsgqusf1olem1  33703  lmicqusker  33708  ricqusker  33716  elrspunidl  33717  elrspunsn  33718  zringfrac  33825  0mplric  33886  selvply1rhmlemb  33890  selvply1rhmlem3  33893  selvply1rhmlem5  33895  selvply1rhm  33896  mplidom  33899  mplvrpmga  33916  mplvrpmrhm  33918  psrgsum  33919  psrmonmul  33921  psrmonprod  33923  splysubrg  33931  issply  33932  esplyfvaln  33945  vietalem  33950  vieta  33951  ply1degltdim  33994  lbsdiflsp0  33997  fedgmullem1  34000  fedgmul  34002  assarrginv  34007  evls1fldgencl  34041  fldextrspunlsplem  34044  fldextrspunlsp  34045  extdgfialglem2  34064  extdgfialg  34065  algextdeglem4  34091  algextdeg  34096  constrcbvlem  34126  madjusmdetlem2  34199  madjusmdet  34202  zartop  34247  zartopon  34248  zart0  34250  zarmxt1  34251  zarcmp  34253  rhmpreimacn  34256  xrge0mulc1cn  34312  xrge0tmd  34316  xrge0tmdALT  34317  cbvesumv  34414  gsumesum  34430  esumlub  34431  esumpcvgval  34449  esumcvg  34457  esumcvg2  34458  eulerpartlems  34731  eulerpart  34753  fibp1  34772  rrvadd  34823  ballotlemfval  34861  ballotlemi  34872  ballotlemsval  34880  ballotlemsv  34881  ballotlemsf1o  34885  ballotlemrval  34889  ballotlemrinv  34905  signsply0  34919  actfunsnf1o  34972  actfunsnrndisj  34973  itgexpif  34974  hgt750lemb  35024  onvf1odlem3  35570  derangfmla  35663  erdsze  35675  pconnpi1  35710  cvmscbv  35731  cvmsss2  35747  cvmliftlem15  35771  cvmlift2  35789  cvmlift3  35801  elmrsubrn  35993  iprodefisum  36214  cbvprodvw2  36740  cbvitgvw2  36741  knoppcnlem7  37069  knoppf  37105  f1omptsn  37964  mptsnun  37966  fin2so  38239  poimirlem27  38279  broucube  38286  ftc1anclem5  38329  ftc1anclem6  38330  sdclem2  38374  prdstotbnd  38426  prdsbnd2  38427  heiborlem10  38452  lshpkrcl  39871  tendoplcbv  41530  tendo0cbv  41541  tendoicbv  41548  lcfl7N  42256  lcf1o  42306  hdmap1cbv  42557  frlmsnic  43291  evlselv  43304  mzpclval  43439  mzpcompact2lem  43465  rmxyval  43625  dnnumch1  43754  aomclem3  43766  aomclem8  43771  dfac21  43776  pwfi2f1o  43806  dftrcl3  44429  dfrtrcl3  44442  rfovcnvf1od  44713  fsovrfovd  44718  fsovcnvlem  44722  dssmapnvod  44729  clsk3nimkb  44749  radcnvrat  45007  expgrowthi  45026  expgrowth  45028  dvradcnv2  45040  binomcxplemradcnv  45045  binomcxplemdvbinom  45046  binomcxplemdvsum  45048  binomcxplemnotnn0  45049  binomcxp  45050  wessf1ornlem  45886  projf1o  45897  fsumsermpt  46278  fmuldfeqlem1  46281  fprodcn  46299  sumnnodd  46329  limsupvaluz  46405  limsupvaluz2  46435  supcnvlimsup  46437  supcnvlimsupmpt  46438  liminfval2  46465  liminflelimsuplem  46472  fprodsubrecnncnv  46605  fprodaddrecnncnv  46607  dvsinax  46610  fperdvper  46616  dvcosax  46623  ioodvbdlimc1lem1  46628  ioodvbdlimc1  46630  ioodvbdlimc2  46632  dvnmul  46640  dvnprodlem1  46643  dvnprodlem2  46644  dvnprodlem3  46645  dvnprod  46646  itgsin0pilem1  46647  itgiccshift  46677  stoweidlem2  46699  stoweidlem17  46714  stoweidlem32  46729  stoweidlem34  46731  stoweidlem43  46740  stirlinglem2  46772  stirlinglem3  46773  stirlinglem8  46778  dirkerval  46788  dirkerval2  46791  dirkeritg  46799  dirkercncflem3  46802  dirkercncf  46804  fourierdlem14  46818  fourierdlem18  46822  fourierdlem53  46856  fourierdlem62  46865  fourierdlem71  46874  fourierdlem74  46877  fourierdlem75  46878  fourierdlem76  46879  fourierdlem80  46883  fourierdlem81  46884  fourierdlem84  46887  fourierdlem88  46891  fourierdlem92  46895  fourierdlem93  46896  fourierdlem94  46897  fourierdlem95  46898  fourierdlem96  46899  fourierdlem97  46900  fourierdlem98  46901  fourierdlem99  46902  fourierdlem101  46904  fourierdlem103  46906  fourierdlem104  46907  fourierdlem105  46908  fourierdlem106  46909  fourierdlem107  46910  fourierdlem108  46911  fourierdlem110  46913  fourierdlem111  46914  fourierdlem112  46915  fourierdlem113  46916  fourierdlem115  46918  fouriersw  46928  elaa2  46931  etransclem1  46932  etransclem5  46936  etransclem6  46937  etransclem11  46942  etransclem13  46944  etransclem41  46972  etransclem47  46978  etransc  46980  ioorrnopn  47002  ioorrnopnxr  47004  subsaliuncl  47055  sge0resplit  47103  sge0fodjrnlem  47113  nnfoctbdj  47153  iundjiun  47157  voliunsge0lem  47169  meaiuninclem  47177  meaiuninc  47178  meaiininclem  47183  meaiininc  47184  omeiunltfirp  47216  carageniuncllem2  47219  carageniuncl  47220  0ome  47226  isomennd  47228  hoicvrrex  47253  ovn0  47263  ovnsubaddlem2  47268  ovnsubadd  47269  sge0hsphoire  47286  hoidmv1lelem3  47290  hoidmv1le  47291  hoidmvlelem1  47292  hoidmvlelem2  47293  hoidmvlelem3  47294  hoidmvlelem4  47295  hoidmvlelem5  47296  hoidmvle  47297  ovnhoilem2  47299  ovnhoi  47300  hspmbllem2  47324  hspmbl  47326  hoimbl  47328  opnvonmbllem2  47330  ovnsubadd2  47343  ovolval4  47348  ovolval5lem3  47351  ovnovollem3  47355  iccvonmbl  47376  vonioolem2  47378  vonioo  47379  vonicclem2  47381  vonicc  47382  smflimlem4  47471  smfsuplem2  47509  smflimsuplem1  47517  smflimsuplem8  47524  smflimsup  47525  fundcmpsurbijinjpreimafv  48139  prproropf1o  48239  isuspgrim0  48642  cycldlenngric  48676  isubgr3stgrlem8  48721  rmsupp0  49131  domnmsuppn0  49132  rmsuppss  49133  suppmptcfin  49139  ply1mulgsum  49153  lcoc0  49185  linc1  49188  lcoel0  49191  lcoss  49199  el0ldep  49229  lincresunit3  49244  isldepslvec2  49248  itcovalpclem2  49434  itcovalt2lem2  49439  amgmlemALT  50586