Theorem mpteq2dva 5205

Description: Slightly more general equality inference for the maps-to notation. (Contributed by Scott Fenton, 25-Apr-2012.) Remove dependency on ax-10 2176. (Revised by SN, 11-Nov-2024.)

Hypothesis

Ref	Expression
mpteq2dva.1	⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 = 𝐶)

Assertion

Ref	Expression
mpteq2dva	⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵) = (𝑥 ∈ 𝐴 ↦ 𝐶))

Distinct variable group:   𝜑,𝑥

Allowed substitution hints:   𝐴(𝑥)   𝐵(𝑥)   𝐶(𝑥)

Proof of Theorem mpteq2dva

Step	Hyp	Ref	Expression
1		eqidd 2764	. 2 ⊢ (𝜑 → 𝐴 = 𝐴)
2		mpteq2dva.1	. 2 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 = 𝐶)
3	1, 2	mpteq12dva 5198	1 ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵) = (𝑥 ∈ 𝐴 ↦ 𝐶))

Syntax hints:   → wi 4   ∧ wa 400   = wceq 1570   ∈ wcel 2143   ↦ 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-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-opab 5175  df-mpt 5194

This theorem is referenced by:  mpteq2dv  5206  mpteq2ia  5207  2fvcoidd  7297  offval  7685  offval2  7696  coof  7700  caofinvl  7708  caofcom  7713  caofass  7716  caofdi  7718  caofdir  7719  caonncan  7720  curry1  8100  curry2  8103  mpocurryd  8266  pw2f1olem  9070  mapxpen  9132  xpmapenlem  9133  cantnfp1  9651  cantnflem1d  9658  cantnflem1  9659  cnfcom2lem  9671  dfac12lem1  10128  seqof  14097  seqof2  14098  swrdswrd  14744  repswswrd  14823  repswrevw  14826  revco  14873  ccatco  14874  repsco  14879  ofccat  15008  lo1eq  15621  rlimeq  15622  lo1mul2  15682  o1dif  15683  lo1sub  15684  rlimdiv  15699  caucvgr  15729  sumeq1  15742  fsumrlim  15865  fsumo1  15866  climfsum  15874  geomulcvg  15932  vdwlem8  17049  prmgapprmo  17123  restid2  17484  pwsplusgval  17545  pwsmulrval  17546  pwsvscafval  17549  qusin  17599  xpsaddlem  17628  xpsvsca  17632  catidd  17737  fuclid  18027  fucrid  18028  fucass  18029  setcepi  18146  prf1st  18261  prf2nd  18262  1st2ndprf  18263  curfcl  18289  curfuncf  18295  diag2  18302  curf2ndf  18304  hof2val  18313  hofcllem  18315  hofcl  18316  yonedalem4a  18332  yonedalem4c  18334  yonedalem3b  18336  yonedainv  18338  yonffthlem  18339  prdssgrpd  18792  prdsidlem  18828  prdsmndd  18829  mhmvlin  18860  pwsco2mhm  18893  frmdup3lem  18926  frmdup3  18927  smndex1gid  18964  smndex1gidOLD  18965  smndex1igidOLD  18967  grpinvpropd  19082  prdsinvlem  19116  pwsinvg  19120  pwssub  19121  galactghm  19475  cayleylem1  19483  pmtrprfval  19558  sylow1lem2  19670  sylow3lem1  19698  efginvrel1  19799  frgpup3lem  19848  frgpup3  19849  prdscmnd  19932  iscyggen  19951  gsumval3  19978  gsumcllem  19979  gsumzsplit  19998  gsumsub  20019  gsummptf1o  20034  gsum2d  20043  gsum2d2  20045  gsumxp  20047  prdsgsum  20052  telgsumfz  20061  telgsumfz0  20063  telgsum  20065  dprdfsub  20094  dprdfeq0  20095  dprddisj2  20112  dprd2d2  20117  dpjidcl  20131  ablfaclem2  20159  ablfac2  20162  prdsmgp  20228  prdsrngd  20255  srgbinomlem3  20311  srgbinomlem4  20312  srgbinomlem  20313  gsumdixp  20401  prdsringd  20403  pwsgprod  20412  prdslmodd  21071  mulgrhm2  21609  frgpcyg  21704  freshmansdream  21705  evpmodpmf1o  21727  phlpropd  21786  frlmphl  21912  uvcresum  21924  frlmup1  21929  asclpropd  22028  psrass1lem  22064  psrlinv  22086  psrass1  22094  psrdi  22095  psrdir  22096  psrass23l  22097  psrcom  22098  psrass23  22099  resspsrmul  22106  mplsubrglem  22134  mplmonmul  22168  mplcoe1  22169  mplcoe5  22172  mplcoe4  22203  evlslem3  22212  evlslem1  22214  evlsvvval  22225  rhmcomulmpl  22256  evlsevl  22264  selvvvval  22274  mhpmulcl  22293  psdmplcl  22306  psdadd  22307  psdmul  22310  psdmvr  22313  psrplusgpropd  22376  psropprmul  22378  coe1mul2  22411  coe1tm  22415  coe1tmmul2  22418  coe1tmmul  22419  coe1pwmul  22421  cply1mul  22437  ply1coe  22439  eqcoe1ply1eq  22440  lply1binomsc  22452  evl1gsummon  22506  evls1fpws  22510  mamures  22535  grpvrinv  22537  mamuass  22540  mamudi  22541  mamudir  22542  mamuvs1  22543  mamuvs2  22544  mpomatmul  22584  mamutpos  22596  madetsumid  22599  dmatmul  22635  scmatscm  22651  1mavmul  22686  mavmulass  22687  mvmumamul1  22692  mulmarep1gsum1  22711  mulmarep1gsum2  22712  mdetleib2  22726  mdetfval1  22728  mdet0pr  22730  mdetdiag  22737  mdetdiagid  22738  mdetrlin  22740  mdetrsca  22741  mdetralt  22746  mdetunilem9  22758  gsummatr01  22797  smadiadetlem1a  22801  smadiadetlem3  22806  smadiadetlem4  22807  cpmatmcllem  22856  mat2pmatmul  22869  decpmatmullem  22909  decpmatmul  22910  pmatcollpw1lem2  22913  pmatcollpw  22919  pmatcollpw3lem  22921  pmatcollpwscmat  22929  idpm2idmp  22939  mp2pm2mplem3  22946  mp2pm2mplem4  22947  mp2pm2mplem5  22948  mp2pm2mp  22949  pm2mpghm  22954  pm2mpmhmlem2  22957  monmat2matmon  22962  pm2mp  22963  chpdmat  22979  chpscmat  22980  chpscmatgsumbin  22982  chpscmatgsummon  22983  chp0mat  22984  chpidmat  22985  chfacfscmulgsum  22998  chfacfpmmulgsum  23002  chfacfpmmulgsum2  23003  cayhamlem1  23004  cpmidgsumm2pm  23007  cpmidpmat  23011  cpmadugsumlemB  23012  cpmadugsumlemC  23013  cpmadugsumlemF  23014  cpmadumatpoly  23021  cayhamlem3  23025  cayhamlem4  23026  cayleyhamilton0  23027  cayleyhamiltonALT  23029  neiptopnei  23270  neiptopreu  23271  ptcnplem  23759  cnmpt1t  23803  cnmpt12  23805  cnmptkp  23818  cnmptk1  23819  cnmpt1k  23820  cnmptkk  23821  cnmptk1p  23823  cnmpt2k  23826  qtopeu  23854  pt1hmeo  23944  ptunhmeo  23946  xkocnv  23952  xkohmeo  23953  flfcnp2  24145  cnmpt1plusg  24225  istgp2  24229  tmdmulg  24230  tgpmulg  24231  tmdgsum  24233  subgtgp  24243  symgtgp  24244  tgpconncomp  24251  prdstgpd  24263  tsmsmhm  24284  tsmsadd  24285  tsmssub  24287  tgptsmscls  24288  tsmssplit  24290  tsmsxplem1  24291  tsmsxplem2  24292  cnmpt1vsca  24332  tlmtgp  24334  ustuqtoplem  24377  utopsnneip  24386  ressprdsds  24509  metuval  24687  nmfval0  24728  tngnm  24789  nmoeq0  24874  idnghm  24881  cnmpt1ds  24981  fsumcn  25010  expcn  25012  divccn  25013  divccncf  25046  negcncf  25062  copco  25158  pcopt  25162  pcopt2  25163  pcoass  25164  pi1xfrcnvlem  25196  cnmpt1ip  25387  rrxnm  25531  rrxds  25533  minveclem3b  25568  divcncf  25587  ovolctb  25630  ovoliunnul  25647  voliunlem3  25692  ovolfs2  25711  uniioombllem2  25723  vitalilem4  25751  vitalilem5  25752  ismbf  25768  mbfss  25786  mbfmulc2re  25788  mbfneg  25790  mbfpos  25791  mbfposb  25793  mbfadd  25801  mbfsub  25802  mbfmulc2  25803  mbfinf  25805  mbflimsup  25806  mbflimlem  25807  i1fpos  25846  i1fposd  25847  itg1climres  25854  mbfmul  25866  itg2mulc  25887  itg2i1fseq  25895  itg2cnlem1  25901  itg2cnlem2  25902  itgresr  25919  iblneg  25943  i1fibl  25948  itgitg1  25949  iblsub  25962  itgfsum  25967  itgmulc2lem1  25972  limcmpt  26023  limccnp  26031  limcco  26033  dvreslem  26049  dvres2lem  26050  dvidlem  26055  dvcnp2  26060  dvaddbr  26078  dvmulbr  26079  dvmulf  26083  dvcmulf  26085  dvcobr  26086  dvcof  26088  dvcjbr  26089  dvcj  26090  dvfre  26091  dvexp  26093  dvexp2  26094  dvrec  26095  dvmptcmul  26104  dvmptdivc  26105  dvmptneg  26106  dvmptsub  26107  dvmptre  26109  dvmptim  26110  dvrecg  26113  dvmptdiv  26114  dvmptfsum  26115  dvcnvlem  26116  dvcnv  26117  dvexp3  26118  dvef  26120  dvsincos  26121  dv11cn  26141  lhop2  26155  lhop  26156  ftc2  26184  itgparts  26187  itgsubstlem  26188  mdegfval  26200  mdegmullem  26216  ply1termlem  26341  plypow  26343  plyconst  26344  plyeq0lem  26348  plypf1  26350  plyaddlem1  26351  plymullem1  26352  coeeulem  26362  coeidlem  26375  plyco  26379  coeeq2  26380  0dgr  26383  0dgrb  26384  dgrcolem1  26411  dgrcolem2  26412  plycjlem  26414  plymul02  26422  plyn0mulidp  26423  plymulidp  26424  dvply1  26426  dvply2g  26427  plydiveu  26440  plyremlem  26446  elqaalem3  26463  taylfval  26503  dvtaylp  26514  taylthlem1  26517  taylthlem2  26518  ulmshft  26534  mtestbdd  26549  iblulm  26551  itgulm2  26553  pserulm  26566  psercn2  26567  pserdvlem2  26572  pserdv  26573  pserdv2  26574  abelthlem1  26575  abelthlem3  26577  advlog  26800  advlogexp  26801  dvcxp1  26886  dvcxp2  26887  dvcncxp1  26889  sqrtcn  26896  loglesqrt  26907  dvatan  27081  atantayl2  27084  atantayl3  27085  leibpi  27088  rlimcnp2  27112  efrlim  27115  dfef2  27116  cxp2lim  27122  divsqrtsumlem  27125  lgamgulmlem2  27175  lgamgulm2  27181  lgamcvglem  27185  gamcvg2lem  27204  ftalem7  27224  basellem9  27234  muinv  27338  logfacrlim  27369  logexprlim  27370  dchrmullid  27397  dchrinvcl  27398  lgseisenlem3  27522  lgseisenlem4  27523  chtppilimlem2  27619  chebbnd2  27622  chpchtlim  27624  chpo1ub  27625  rpvmasumlem  27632  dchrmusumlema  27638  dchrvmasumlem1  27640  dchrvmasumiflem2  27647  dchrisum0fno1  27656  rpvmasum2  27657  dchrisum0lema  27659  dchrisum0lem1  27661  dchrisum0lem2a  27662  dchrisum0lem2  27663  dchrisum0  27665  dchrmusumlem  27667  dchrvmasumlem  27668  rpvmasum  27671  rplogsum  27672  logdivsum  27678  mulog2sumlem3  27681  vmalogdivsum2  27683  vmalogdivsum  27684  2vmadivsumlem  27685  logsqvma2  27688  log2sumbnd  27689  selberglem2  27691  selberg3lem1  27702  selberg3  27704  selberg4lem1  27705  selberg4  27706  pntrsumo1  27710  selberg3r  27714  selberg4r  27715  selberg34r  27716  pntrlog2bndlem2  27723  pntrlog2bndlem4  27725  pntrlog2bndlem5  27726  pntrlog2bndlem6  27728  padicabvf  27776  padicabvcxp  27777  mirval  28913  crctcshlem4  30150  clwlknf1oclwwlkn  30416  eucrct2eupth  30577  chscllem4  31973  brafnmul  32284  kbmul  32288  cofmpt2  32960  ofresid  32968  ofoprabco  32990  fmptunsnop  33026  fcobijfs  33047  fcobijfs2  33048  gsummpt2d  33350  gsummptres  33353  gsummptres2  33354  gsummptf1od  33356  gsummptp1  33358  gsummptfsf1o  33361  gsumfs2d  33362  gsumpart  33364  gsumhashmul  33368  gsummulsubdishift1  33369  gsummulsubdishift2  33370  gsumwrd2dccat  33379  fzto1st1  33403  fzto1st  33404  elrgspnlem1  33543  elrgspnlem2  33544  elrgspnlem3  33545  elrgspnlem4  33546  elrgspnsubrunlem1  33548  elrgspnsubrunlem2  33549  qusbas2  33696  qusima  33698  elrspunidl  33717  elrspunsn  33718  rprmdvdsprod  33805  ressply1evls1  33836  evl1deg1  33847  evl1deg2  33848  evl1deg3  33849  gsummoncoe1fzo  33868  mplasclco  33887  selvply1rhmlemb  33890  selvply1rhmlem2  33892  selvply1rhmlem4  33894  selvply1rhm0  33897  mplmulmvr  33910  evlextv  33913  mplvrpmga  33916  mplvrpmmhm  33917  mplvrpmrhm  33918  psrgsum  33919  psrmonmul  33921  issply  33932  esplyfval0  33935  esplyfval3  33943  esplyfval1  33944  esplyfvaln  33945  esplyind  33946  vietalem  33950  lbsdiflsp0  33997  fedgmullem1  34000  fedgmullem2  34001  fldextrspunlsplem  34044  fldextrspunlsp  34045  extdgfialglem2  34064  mdetpmtr1  34194  mdetlap  34203  xrge0mulc1cn  34312  esumval  34417  esumsnf  34435  esumpcvgval  34449  esumcvg  34457  esumcvgsum  34459  esumsup  34460  ofcfeqd2  34472  meascnbl  34590  sitgval  34703  probmeasb  34801  cndprobprob  34809  dstfrvclim1  34849  ballotlemfval  34861  ballotlemsval  34880  ballotlemieq  34888  signsplypnf  34918  signstfv  34931  signstfvn  34937  signstfvp  34939  itgexpif  34974  logdivsqrle  35018  ptpconn  35706  cvmliftlem6  35763  cvmliftphtlem  35790  cvmlift3lem5  35796  elmrsubrn  35993  msubfval  35997  msubco  36004  divcnvlin  36206  knoppcnlem9  37071  knoppcnlem10  37072  knoppcnlem11  37073  bj-finsumval0  37910  curf  38230  matunitlindflem1  38248  matunitlindflem2  38249  poimirlem3  38255  poimirlem15  38267  poimirlem16  38268  poimirlem17  38269  poimirlem19  38271  poimirlem20  38272  broucube  38286  ovoliunnfl  38294  voliunnfl  38296  volsupnfl  38297  mbfposadd  38299  itg2addnclem  38303  itg2addnclem3  38305  itg2addnc  38306  itgaddnclem2  38311  itgaddnc  38312  iblsubnc  38313  itgsubnc  38314  itgmulc2nclem1  38318  itgmulc2nclem2  38319  itgmulc2nc  38320  itgabsnc  38321  ftc1cnnclem  38323  ftc1anclem3  38327  ftc1anclem5  38329  ftc1anclem6  38330  ftc1anclem8  38332  ftc1anc  38333  ftc2nc  38334  areacirclem1  38340  areacirclem2  38341  areacirclem4  38343  areacirc  38345  upixp  38361  lcmineqlem8  42784  lcmineqlem12  42788  dvrelog2b  42814  dvrelogpow2b  42816  aks4d1p1p6  42821  aks4d1p1p5  42823  aks6d1c1  42864  aks6d1c5lem3  42885  sticksstones12a  42905  sticksstones12  42906  sticksstones19  42913  aks6d1c6lem1  42918  aks6d1c6lem4  42921  aks6d1c7lem3  42930  qsalrel  42990  rhmcomulpsr  43297  evlselv  43304  fsuppssindlem1  43306  fsuppssind  43308  mhphf  43312  mzpsubst  43462  mzprename  43463  mzpcompact2lem  43465  eldioph2  43476  rabdiophlem2  43512  mendlmod  43899  mendassa  43900  areaquad  43926  fsovcnvlem  44722  hashnzfzclim  45015  expgrowthi  45026  expgrowth  45028  uzmptshftfval  45039  dvradcnv2  45040  binomcxplemrat  45043  binomcxplemfrat  45044  binomcxplemradcnv  45045  binomcxplemdvbinom  45046  binomcxplemcvg  45047  binomcxplemdvsum  45048  binomcxplemnotnn0  45049  mulc1cncfg  46288  expcnfg  46290  fprodcnlem  46298  clim1fr1  46300  divcnvg  46326  sublimc  46349  reclimc  46350  divlimc  46353  limsupresico  46397  limsuppnfdlem  46398  limsupvaluz  46405  supcnvlimsupmpt  46438  liminfresico  46468  climliminflimsupd  46498  cncfmptssg  46568  negcncfg  46578  cncficcgt0  46585  fprodcncf  46597  fprodsubrecnncnvlem  46604  fprodaddrecnncnvlem  46606  dvsinax  46610  dvasinbx  46617  dvdivf  46619  ioodvbdlimc1lem2  46629  ioodvbdlimc2lem  46631  dvnmptdivc  46635  dvxpaek  46637  dvnxpaek  46639  dvnmul  46640  dvnprodlem2  46644  ibliccsinexp  46648  itgsinexplem1  46651  itgsinexp  46652  iblempty  46662  itgcoscmulx  46666  itgsincmulx  46671  itgioocnicc  46674  iblcncfioo  46675  itgsbtaddcnst  46679  volioofmpt  46691  volicofmpt  46694  stoweidlem4  46701  stirlinglem5  46775  dirkerval  46788  dirkertrigeq  46798  dirkeritg  46799  dirkercncflem2  46801  dirkercncflem4  46803  fourierdlem16  46820  fourierdlem18  46822  fourierdlem21  46825  fourierdlem22  46826  fourierdlem28  46832  fourierdlem39  46843  fourierdlem40  46844  fourierdlem41  46845  fourierdlem53  46856  fourierdlem56  46859  fourierdlem57  46860  fourierdlem60  46863  fourierdlem61  46864  fourierdlem68  46871  fourierdlem73  46876  fourierdlem74  46877  fourierdlem75  46878  fourierdlem76  46879  fourierdlem78  46881  fourierdlem81  46884  fourierdlem82  46885  fourierdlem83  46886  fourierdlem84  46887  fourierdlem85  46888  fourierdlem88  46891  fourierdlem90  46893  fourierdlem92  46895  fourierdlem93  46896  fourierdlem95  46898  fourierdlem97  46900  fourierdlem101  46904  fourierdlem103  46906  fourierdlem104  46907  fourierdlem111  46914  fourierdlem112  46915  sqwvfoura  46925  sqwvfourb  46926  fouriersw  46928  elaa2lem  46930  etransclem4  46935  etransclem17  46948  etransclem18  46949  etransclem32  46963  etransclem46  46977  sge0z  47072  sge0revalmpt  47075  sge0tsms  47077  sge0sup  47088  sge0iunmptlemre  47112  sge0iun  47116  sge0xaddlem2  47131  ismeannd  47164  psmeasurelem  47167  meaiuninclem  47177  meaiininclem  47183  caratheodory  47225  isomenndlem  47227  ovnval  47238  hoicvrrex  47253  ovnlecvr  47255  ovncvrrp  47261  ovn0lem  47262  ovnsubaddlem1  47267  hoidmv1lelem2  47289  hoidmv1le  47291  hoidmvlelem3  47294  ovnhoilem2  47299  ovnhoi  47300  ovnlecvr2  47307  ovncvr2  47308  hspmbllem2  47324  ovolval2lem  47340  ovolval3  47344  ovolval5lem1  47349  ovolval5lem2  47350  ovnovollem1  47353  ovnovollem2  47354  vonioolem1  47377  vonicclem1  47380  vonct  47390  smflim  47474  smfinflem  47514  smflimsuplem5  47521  smfliminflem  47527  cfsetsnfsetfv  47777  fundcmpsurbijinjpreimafv  48139  fundcmpsurinjimaid  48143  fdmdifeqresdif  49105  ply1mulgsumlem2  49150  lincvalsc0  49184  linc0scn0  49186  lincdifsn  49187  lincsum  49192  lincscm  49193  lindslinindimp2lem4  49224  lindslinindsimp2lem5  49225  lincresunit3lem2  49243  1arymaptfo  49406  itcovalpclem1  49433  itcovalpclem2  49434  itcovalt2lem1  49438  itcovalt2lem2  49439  tposcurf1  50060  tposcurf2  50061  diag1  50065  fuco22  50100  fucocolem2  50115  fucocolem3  50116  fucocolem4  50117  fucoco  50118  fucolid  50122  fucorid  50123  postcofval  50125  precofval  50128  precofvalALT  50129  precofval2  50130  fucoppcco  50170  islmd  50426  iscmd  50427  aacllem  50584  amgmwlem  50585