Theorem mpteq2dva 5266

Description: Slightly more general equality inference for the maps-to notation. (Contributed by Scott Fenton, 25-Apr-2012.) Remove dependency on ax-10 2141. (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 2741	. 2 ⊢ (𝜑 → 𝐴 = 𝐴)
2		mpteq2dva.1	. 2 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 = 𝐶)
3	1, 2	mpteq12dva 5255	1 ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵) = (𝑥 ∈ 𝐴 ↦ 𝐶))

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1537   ∈ wcel 2108   ↦ cmpt 5249

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-opab 5229  df-mpt 5250

This theorem is referenced by:  mpteq2dv  5268  mpteq2ia  5269  2fvcoidd  7333  offval  7723  offval2  7734  coof  7737  caofinvl  7745  caofcom  7750  caofass  7752  caofdi  7754  caofdir  7755  caonncan  7756  curry1  8145  curry2  8148  mpocurryd  8310  pw2f1olem  9142  mapxpen  9209  xpmapenlem  9210  cantnfp1  9750  cantnflem1d  9757  cantnflem1  9758  cnfcom2lem  9770  dfac12lem1  10213  seqof  14110  seqof2  14111  swrdswrd  14753  repswswrd  14832  repswrevw  14835  revco  14883  ccatco  14884  repsco  14889  ofccat  15018  lo1eq  15614  rlimeq  15615  lo1mul2  15675  o1dif  15676  lo1sub  15677  rlimdiv  15694  caucvgr  15724  sumeq1  15737  fsumrlim  15859  fsumo1  15860  climfsum  15868  geomulcvg  15924  vdwlem8  17035  prmgapprmo  17109  restid2  17490  pwsplusgval  17550  pwsmulrval  17551  pwsvscafval  17554  qusin  17604  xpsaddlem  17633  xpsvsca  17637  catidd  17738  fuclid  18036  fucrid  18037  fucass  18038  setcepi  18155  prf1st  18273  prf2nd  18274  1st2ndprf  18275  curfcl  18302  curfuncf  18308  diag2  18315  curf2ndf  18317  hof2val  18326  hofcllem  18328  hofcl  18329  yonedalem4a  18345  yonedalem4c  18347  yonedalem3b  18349  yonedainv  18351  yonffthlem  18352  prdssgrpd  18771  prdsidlem  18804  prdsmndd  18805  mhmvlin  18836  pwsco2mhm  18868  frmdup3lem  18901  frmdup3  18902  smndex1gid  18938  smndex1igid  18939  grpinvpropd  19055  prdsinvlem  19089  pwsinvg  19093  pwssub  19094  galactghm  19446  cayleylem1  19454  pmtrprfval  19529  sylow1lem2  19641  sylow3lem1  19669  efginvrel1  19770  frgpup3lem  19819  frgpup3  19820  prdscmnd  19903  iscyggen  19922  gsumval3  19949  gsumcllem  19950  gsumzsplit  19969  gsumsub  19990  gsummptf1o  20005  gsum2d  20014  gsum2d2  20016  gsumxp  20018  prdsgsum  20023  telgsumfz  20032  telgsumfz0  20034  telgsum  20036  dprdfsub  20065  dprdfeq0  20066  dprddisj2  20083  dprd2d2  20088  dpjidcl  20102  ablfaclem2  20130  ablfac2  20133  prdsmgp  20178  prdsrngd  20203  srgbinomlem3  20255  srgbinomlem4  20256  srgbinomlem  20257  gsumdixp  20342  prdsringd  20344  prdslmodd  20990  mulgrhm2  21512  frgpcyg  21615  freshmansdream  21616  evpmodpmf1o  21637  phlpropd  21696  frlmphl  21824  uvcresum  21836  frlmup1  21841  asclpropd  21940  psrass1lem  21975  psrlinv  21998  psrass1  22007  psrdi  22008  psrdir  22009  psrass23l  22010  psrcom  22011  psrass23  22012  resspsrmul  22019  mplsubrglem  22047  mplmonmul  22077  mplcoe1  22078  mplcoe5  22081  mplcoe4  22118  evlslem3  22127  evlslem1  22129  mhpmulcl  22176  psdmplcl  22189  psdadd  22190  psdmul  22193  psrplusgpropd  22258  psropprmul  22260  coe1mul2  22293  coe1tm  22297  coe1tmmul2  22300  coe1tmmul  22301  coe1pwmul  22303  cply1mul  22321  ply1coe  22323  eqcoe1ply1eq  22324  lply1binomsc  22336  evl1gsummon  22390  evls1fpws  22394  rhmcomulmpl  22407  mamures  22422  grpvrinv  22424  mamuass  22427  mamudi  22428  mamudir  22429  mamuvs1  22430  mamuvs2  22431  mpomatmul  22473  mamutpos  22485  madetsumid  22488  dmatmul  22524  scmatscm  22540  1mavmul  22575  mavmulass  22576  mvmumamul1  22581  mulmarep1gsum1  22600  mulmarep1gsum2  22601  mdetleib2  22615  mdetfval1  22617  mdet0pr  22619  mdetdiag  22626  mdetdiagid  22627  mdetrlin  22629  mdetrsca  22630  mdetralt  22635  mdetunilem9  22647  gsummatr01  22686  smadiadetlem1a  22690  smadiadetlem3  22695  smadiadetlem4  22696  cpmatmcllem  22745  mat2pmatmul  22758  decpmatmullem  22798  decpmatmul  22799  pmatcollpw1lem2  22802  pmatcollpw  22808  pmatcollpw3lem  22810  pmatcollpwscmat  22818  idpm2idmp  22828  mp2pm2mplem3  22835  mp2pm2mplem4  22836  mp2pm2mplem5  22837  mp2pm2mp  22838  pm2mpghm  22843  pm2mpmhmlem2  22846  monmat2matmon  22851  pm2mp  22852  chpdmat  22868  chpscmat  22869  chpscmatgsumbin  22871  chpscmatgsummon  22872  chp0mat  22873  chpidmat  22874  chfacfscmulgsum  22887  chfacfpmmulgsum  22891  chfacfpmmulgsum2  22892  cayhamlem1  22893  cpmidgsumm2pm  22896  cpmidpmat  22900  cpmadugsumlemB  22901  cpmadugsumlemC  22902  cpmadugsumlemF  22903  cpmadumatpoly  22910  cayhamlem3  22914  cayhamlem4  22915  cayleyhamilton0  22916  cayleyhamiltonALT  22918  neiptopnei  23161  neiptopreu  23162  ptcnplem  23650  cnmpt1t  23694  cnmpt12  23696  cnmptkp  23709  cnmptk1  23710  cnmpt1k  23711  cnmptkk  23712  cnmptk1p  23714  cnmpt2k  23717  qtopeu  23745  pt1hmeo  23835  ptunhmeo  23837  xkocnv  23843  xkohmeo  23844  flfcnp2  24036  cnmpt1plusg  24116  istgp2  24120  tmdmulg  24121  tgpmulg  24122  tmdgsum  24124  subgtgp  24134  symgtgp  24135  tgpconncomp  24142  prdstgpd  24154  tsmsmhm  24175  tsmsadd  24176  tsmssub  24178  tgptsmscls  24179  tsmssplit  24181  tsmsxplem1  24182  tsmsxplem2  24183  cnmpt1vsca  24223  tlmtgp  24225  ustuqtoplem  24269  utopsnneip  24278  ressprdsds  24402  metuval  24583  nmfval0  24624  tngnm  24693  nmoeq0  24778  idnghm  24785  cnmpt1ds  24883  fsumcn  24913  expcn  24915  divccn  24916  expcnOLD  24917  divccnOLD  24918  divccncf  24951  negcncf  24967  negcncfOLD  24968  copco  25070  pcopt  25074  pcopt2  25075  pcoass  25076  pi1xfrcnvlem  25108  cnmpt1ip  25300  rrxnm  25444  rrxds  25446  minveclem3b  25481  divcncf  25501  ovolctb  25544  ovoliunnul  25561  voliunlem3  25606  ovolfs2  25625  uniioombllem2  25637  vitalilem4  25665  vitalilem5  25666  ismbf  25682  mbfss  25700  mbfmulc2re  25702  mbfneg  25704  mbfpos  25705  mbfposb  25707  mbfadd  25715  mbfsub  25716  mbfmulc2  25717  mbfinf  25719  mbflimsup  25720  mbflimlem  25721  i1fpos  25761  i1fposd  25762  itg1climres  25769  mbfmul  25781  itg2mulc  25802  itg2i1fseq  25810  itg2cnlem1  25816  itg2cnlem2  25817  itgresr  25834  iblneg  25858  i1fibl  25863  itgitg1  25864  iblsub  25877  itgfsum  25882  itgmulc2lem1  25887  limcmpt  25938  limccnp  25946  limcco  25948  dvreslem  25964  dvres2lem  25965  dvidlem  25970  dvcnp2  25975  dvcnp2OLD  25976  dvaddbr  25994  dvmulbr  25995  dvmulbrOLD  25996  dvmulf  26000  dvcmulf  26002  dvcobr  26003  dvcobrOLD  26004  dvcof  26006  dvcjbr  26007  dvcj  26008  dvfre  26009  dvexp  26011  dvexp2  26012  dvrec  26013  dvmptcmul  26022  dvmptdivc  26023  dvmptneg  26024  dvmptsub  26025  dvmptre  26027  dvmptim  26028  dvrecg  26031  dvmptdiv  26032  dvmptfsum  26033  dvcnvlem  26034  dvcnv  26035  dvexp3  26036  dvef  26038  dvsincos  26039  dv11cn  26060  lhop2  26074  lhop  26075  ftc2  26105  itgparts  26108  itgsubstlem  26109  mdegfval  26121  mdegmullem  26137  ply1termlem  26262  plypow  26264  plyconst  26265  plyeq0lem  26269  plypf1  26271  plyaddlem1  26272  plymullem1  26273  coeeulem  26283  coeidlem  26296  plyco  26300  coeeq2  26301  0dgr  26304  0dgrb  26305  dgrcolem1  26333  dgrcolem2  26334  plycjlem  26336  dvply1  26343  dvply2g  26344  dvply2gOLD  26345  plydiveu  26358  plyremlem  26364  elqaalem3  26381  taylfval  26418  dvtaylp  26430  taylthlem1  26433  taylthlem2  26434  taylthlem2OLD  26435  ulmshft  26451  mtestbdd  26466  iblulm  26468  itgulm2  26470  pserulm  26483  psercn2  26484  psercn2OLD  26485  pserdvlem2  26490  pserdv  26491  pserdv2  26492  abelthlem1  26493  abelthlem3  26495  advlog  26714  advlogexp  26715  dvcxp1  26800  dvcxp2  26801  dvcncxp1  26803  sqrtcn  26811  loglesqrt  26822  dvatan  26996  atantayl2  26999  atantayl3  27000  leibpi  27003  rlimcnp2  27027  efrlim  27030  efrlimOLD  27031  dfef2  27032  cxp2lim  27038  divsqrtsumlem  27041  lgamgulmlem2  27091  lgamgulm2  27097  lgamcvglem  27101  gamcvg2lem  27120  ftalem7  27140  basellem9  27150  muinv  27254  logfacrlim  27286  logexprlim  27287  dchrmullid  27314  dchrinvcl  27315  lgseisenlem3  27439  lgseisenlem4  27440  chtppilimlem2  27536  chebbnd2  27539  chpchtlim  27541  chpo1ub  27542  rpvmasumlem  27549  dchrmusumlema  27555  dchrvmasumlem1  27557  dchrvmasumiflem2  27564  dchrisum0fno1  27573  rpvmasum2  27574  dchrisum0lema  27576  dchrisum0lem1  27578  dchrisum0lem2a  27579  dchrisum0lem2  27580  dchrisum0  27582  dchrmusumlem  27584  dchrvmasumlem  27585  rpvmasum  27588  rplogsum  27589  logdivsum  27595  mulog2sumlem3  27598  vmalogdivsum2  27600  vmalogdivsum  27601  2vmadivsumlem  27602  logsqvma2  27605  log2sumbnd  27606  selberglem2  27608  selberg3lem1  27619  selberg3  27621  selberg4lem1  27622  selberg4  27623  pntrsumo1  27627  selberg3r  27631  selberg4r  27632  selberg34r  27633  pntrlog2bndlem2  27640  pntrlog2bndlem4  27642  pntrlog2bndlem5  27643  pntrlog2bndlem6  27645  padicabvf  27693  padicabvcxp  27694  mirval  28681  crctcshlem4  29853  clwlknf1oclwwlkn  30116  eucrct2eupth  30277  chscllem4  31672  brafnmul  31983  kbmul  31987  cofmpt2  32653  ofresid  32661  ofoprabco  32682  fcobijfs  32737  gsummpt2d  33032  gsummptres  33035  gsummptres2  33036  gsumpart  33038  gsumhashmul  33040  fzto1st1  33095  fzto1st  33096  qusbas2  33399  qusima  33401  elrspunidl  33421  elrspunsn  33422  rprmdvdsprod  33527  evl1deg1  33566  evl1deg2  33567  evl1deg3  33568  gsummoncoe1fzo  33583  lbsdiflsp0  33639  fedgmullem1  33642  fedgmullem2  33643  mdetpmtr1  33769  mdetlap  33778  xrge0mulc1cn  33887  esumval  34010  esumsnf  34028  esumpcvgval  34042  esumcvg  34050  esumcvgsum  34052  esumsup  34053  ofcfeqd2  34065  meascnbl  34183  sitgval  34297  probmeasb  34395  cndprobprob  34403  dstfrvclim1  34442  ballotlemfval  34454  ballotlemsval  34473  ballotlemieq  34481  plymul02  34523  plymulx0  34524  plymulx  34525  signsplypnf  34527  signstfv  34540  signstfvn  34546  signstfvp  34548  itgexpif  34583  logdivsqrle  34627  ptpconn  35201  cvmliftlem6  35258  cvmliftphtlem  35285  cvmlift3lem5  35291  elmrsubrn  35488  msubfval  35492  msubco  35499  divcnvlin  35695  knoppcnlem9  36467  knoppcnlem10  36468  knoppcnlem11  36469  bj-finsumval0  37251  curf  37558  matunitlindflem1  37576  matunitlindflem2  37577  poimirlem3  37583  poimirlem15  37595  poimirlem16  37596  poimirlem17  37597  poimirlem19  37599  poimirlem20  37600  broucube  37614  ovoliunnfl  37622  voliunnfl  37624  volsupnfl  37625  mbfposadd  37627  itg2addnclem  37631  itg2addnclem3  37633  itg2addnc  37634  itgaddnclem2  37639  itgaddnc  37640  iblsubnc  37641  itgsubnc  37642  itgmulc2nclem1  37646  itgmulc2nclem2  37647  itgmulc2nc  37648  itgabsnc  37649  ftc1cnnclem  37651  ftc1anclem3  37655  ftc1anclem5  37657  ftc1anclem6  37658  ftc1anclem8  37660  ftc1anc  37661  ftc2nc  37662  areacirclem1  37668  areacirclem2  37669  areacirclem4  37671  areacirc  37673  upixp  37689  lcmineqlem8  41993  lcmineqlem12  41997  dvrelog2b  42023  dvrelogpow2b  42025  aks4d1p1p6  42030  aks4d1p1p5  42032  aks6d1c1  42073  aks6d1c5lem3  42094  sticksstones12a  42114  sticksstones12  42115  sticksstones19  42122  aks6d1c6lem1  42127  aks6d1c6lem4  42130  aks6d1c7lem3  42139  qsalrel  42235  pwsgprod  42499  rhmcomulpsr  42506  evlsvvval  42518  evlsevl  42526  selvvvval  42540  evlselv  42542  fsuppssindlem1  42546  fsuppssind  42548  mhphf  42552  mzpsubst  42704  mzprename  42705  mzpcompact2lem  42707  eldioph2  42718  rabdiophlem2  42758  mendlmod  43150  mendassa  43151  areaquad  43177  fsovcnvlem  43975  hashnzfzclim  44291  expgrowthi  44302  expgrowth  44304  uzmptshftfval  44315  dvradcnv2  44316  binomcxplemrat  44319  binomcxplemfrat  44320  binomcxplemradcnv  44321  binomcxplemdvbinom  44322  binomcxplemcvg  44323  binomcxplemdvsum  44324  binomcxplemnotnn0  44325  mulc1cncfg  45510  expcnfg  45512  fprodcnlem  45520  clim1fr1  45522  divcnvg  45548  sublimc  45573  reclimc  45574  divlimc  45577  limsupresico  45621  limsuppnfdlem  45622  limsupvaluz  45629  supcnvlimsupmpt  45662  liminfresico  45692  climliminflimsupd  45722  cncfmptssg  45792  negcncfg  45802  cncficcgt0  45809  fprodcncf  45821  fprodsubrecnncnvlem  45828  fprodaddrecnncnvlem  45830  dvsinax  45834  dvasinbx  45841  dvdivf  45843  ioodvbdlimc1lem2  45853  ioodvbdlimc2lem  45855  dvnmptdivc  45859  dvxpaek  45861  dvnxpaek  45863  dvnmul  45864  dvnprodlem2  45868  ibliccsinexp  45872  itgsinexplem1  45875  itgsinexp  45876  iblempty  45886  itgcoscmulx  45890  itgsincmulx  45895  itgioocnicc  45898  iblcncfioo  45899  itgsbtaddcnst  45903  volioofmpt  45915  volicofmpt  45918  stoweidlem4  45925  stirlinglem5  45999  dirkerval  46012  dirkertrigeq  46022  dirkeritg  46023  dirkercncflem2  46025  dirkercncflem4  46027  fourierdlem16  46044  fourierdlem18  46046  fourierdlem21  46049  fourierdlem22  46050  fourierdlem28  46056  fourierdlem39  46067  fourierdlem40  46068  fourierdlem41  46069  fourierdlem53  46080  fourierdlem56  46083  fourierdlem57  46084  fourierdlem60  46087  fourierdlem61  46088  fourierdlem68  46095  fourierdlem73  46100  fourierdlem74  46101  fourierdlem75  46102  fourierdlem76  46103  fourierdlem78  46105  fourierdlem81  46108  fourierdlem82  46109  fourierdlem83  46110  fourierdlem84  46111  fourierdlem85  46112  fourierdlem88  46115  fourierdlem90  46117  fourierdlem92  46119  fourierdlem93  46120  fourierdlem95  46122  fourierdlem97  46124  fourierdlem101  46128  fourierdlem103  46130  fourierdlem104  46131  fourierdlem111  46138  fourierdlem112  46139  sqwvfoura  46149  sqwvfourb  46150  fouriersw  46152  elaa2lem  46154  etransclem4  46159  etransclem17  46172  etransclem18  46173  etransclem32  46187  etransclem46  46201  sge0z  46296  sge0revalmpt  46299  sge0tsms  46301  sge0sup  46312  sge0iunmptlemre  46336  sge0iun  46340  sge0xaddlem2  46355  ismeannd  46388  psmeasurelem  46391  meaiuninclem  46401  meaiininclem  46407  caratheodory  46449  isomenndlem  46451  ovnval  46462  hoicvrrex  46477  ovnlecvr  46479  ovncvrrp  46485  ovn0lem  46486  ovnsubaddlem1  46491  hoidmv1lelem2  46513  hoidmv1le  46515  hoidmvlelem3  46518  ovnhoilem2  46523  ovnhoi  46524  ovnlecvr2  46531  ovncvr2  46532  hspmbllem2  46548  ovolval2lem  46564  ovolval3  46568  ovolval5lem1  46573  ovolval5lem2  46574  ovnovollem1  46577  ovnovollem2  46578  vonioolem1  46601  vonicclem1  46604  vonct  46614  smflim  46698  smfinflem  46738  smflimsuplem5  46745  smfliminflem  46751  cfsetsnfsetfv  46972  fundcmpsurbijinjpreimafv  47281  fundcmpsurinjimaid  47285  fdmdifeqresdif  48066  ply1mulgsumlem2  48116  lincvalsc0  48150  linc0scn0  48152  lincdifsn  48153  lincsum  48158  lincscm  48159  lindslinindimp2lem4  48190  lindslinindsimp2lem5  48191  lincresunit3lem2  48209  1arymaptfo  48377  itcovalpclem1  48404  itcovalpclem2  48405  itcovalt2lem1  48409  itcovalt2lem2  48410  aacllem  48895  amgmwlem  48896