Theorem mpteq2dva 5188

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

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1540   ∈ wcel 2109   ↦ 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-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-opab 5158  df-mpt 5177

This theorem is referenced by:  mpteq2dv  5189  mpteq2ia  5190  2fvcoidd  7238  offval  7626  offval2  7637  coof  7641  caofinvl  7649  caofcom  7654  caofass  7657  caofdi  7659  caofdir  7660  caonncan  7661  curry1  8044  curry2  8047  mpocurryd  8209  pw2f1olem  9005  mapxpen  9067  xpmapenlem  9068  cantnfp1  9596  cantnflem1d  9603  cantnflem1  9604  cnfcom2lem  9616  dfac12lem1  10057  seqof  13984  seqof2  13985  swrdswrd  14629  repswswrd  14708  repswrevw  14711  revco  14759  ccatco  14760  repsco  14765  ofccat  14894  lo1eq  15493  rlimeq  15494  lo1mul2  15554  o1dif  15555  lo1sub  15556  rlimdiv  15571  caucvgr  15601  sumeq1  15614  fsumrlim  15736  fsumo1  15737  climfsum  15745  geomulcvg  15801  vdwlem8  16918  prmgapprmo  16992  restid2  17352  pwsplusgval  17412  pwsmulrval  17413  pwsvscafval  17416  qusin  17466  xpsaddlem  17495  xpsvsca  17499  catidd  17604  fuclid  17894  fucrid  17895  fucass  17896  setcepi  18013  prf1st  18128  prf2nd  18129  1st2ndprf  18130  curfcl  18156  curfuncf  18162  diag2  18169  curf2ndf  18171  hof2val  18180  hofcllem  18182  hofcl  18183  yonedalem4a  18199  yonedalem4c  18201  yonedalem3b  18203  yonedainv  18205  yonffthlem  18206  prdssgrpd  18625  prdsidlem  18661  prdsmndd  18662  mhmvlin  18693  pwsco2mhm  18725  frmdup3lem  18758  frmdup3  18759  smndex1gid  18795  smndex1igid  18796  grpinvpropd  18912  prdsinvlem  18946  pwsinvg  18950  pwssub  18951  galactghm  19301  cayleylem1  19309  pmtrprfval  19384  sylow1lem2  19496  sylow3lem1  19524  efginvrel1  19625  frgpup3lem  19674  frgpup3  19675  prdscmnd  19758  iscyggen  19777  gsumval3  19804  gsumcllem  19805  gsumzsplit  19824  gsumsub  19845  gsummptf1o  19860  gsum2d  19869  gsum2d2  19871  gsumxp  19873  prdsgsum  19878  telgsumfz  19887  telgsumfz0  19889  telgsum  19891  dprdfsub  19920  dprdfeq0  19921  dprddisj2  19938  dprd2d2  19943  dpjidcl  19957  ablfaclem2  19985  ablfac2  19988  prdsmgp  20054  prdsrngd  20079  srgbinomlem3  20131  srgbinomlem4  20132  srgbinomlem  20133  gsumdixp  20222  prdsringd  20224  prdslmodd  20890  mulgrhm2  21403  frgpcyg  21498  freshmansdream  21499  evpmodpmf1o  21521  phlpropd  21580  frlmphl  21706  uvcresum  21718  frlmup1  21723  asclpropd  21822  psrass1lem  21857  psrlinv  21880  psrass1  21889  psrdi  21890  psrdir  21891  psrass23l  21892  psrcom  21893  psrass23  21894  resspsrmul  21901  mplsubrglem  21929  mplmonmul  21959  mplcoe1  21960  mplcoe5  21963  mplcoe4  21994  evlslem3  22003  evlslem1  22005  mhpmulcl  22052  psdmplcl  22065  psdadd  22066  psdmul  22069  psdmvr  22072  psrplusgpropd  22136  psropprmul  22138  coe1mul2  22171  coe1tm  22175  coe1tmmul2  22178  coe1tmmul  22179  coe1pwmul  22181  cply1mul  22199  ply1coe  22201  eqcoe1ply1eq  22202  lply1binomsc  22214  evl1gsummon  22268  evls1fpws  22272  rhmcomulmpl  22285  mamures  22300  grpvrinv  22302  mamuass  22305  mamudi  22306  mamudir  22307  mamuvs1  22308  mamuvs2  22309  mpomatmul  22349  mamutpos  22361  madetsumid  22364  dmatmul  22400  scmatscm  22416  1mavmul  22451  mavmulass  22452  mvmumamul1  22457  mulmarep1gsum1  22476  mulmarep1gsum2  22477  mdetleib2  22491  mdetfval1  22493  mdet0pr  22495  mdetdiag  22502  mdetdiagid  22503  mdetrlin  22505  mdetrsca  22506  mdetralt  22511  mdetunilem9  22523  gsummatr01  22562  smadiadetlem1a  22566  smadiadetlem3  22571  smadiadetlem4  22572  cpmatmcllem  22621  mat2pmatmul  22634  decpmatmullem  22674  decpmatmul  22675  pmatcollpw1lem2  22678  pmatcollpw  22684  pmatcollpw3lem  22686  pmatcollpwscmat  22694  idpm2idmp  22704  mp2pm2mplem3  22711  mp2pm2mplem4  22712  mp2pm2mplem5  22713  mp2pm2mp  22714  pm2mpghm  22719  pm2mpmhmlem2  22722  monmat2matmon  22727  pm2mp  22728  chpdmat  22744  chpscmat  22745  chpscmatgsumbin  22747  chpscmatgsummon  22748  chp0mat  22749  chpidmat  22750  chfacfscmulgsum  22763  chfacfpmmulgsum  22767  chfacfpmmulgsum2  22768  cayhamlem1  22769  cpmidgsumm2pm  22772  cpmidpmat  22776  cpmadugsumlemB  22777  cpmadugsumlemC  22778  cpmadugsumlemF  22779  cpmadumatpoly  22786  cayhamlem3  22790  cayhamlem4  22791  cayleyhamilton0  22792  cayleyhamiltonALT  22794  neiptopnei  23035  neiptopreu  23036  ptcnplem  23524  cnmpt1t  23568  cnmpt12  23570  cnmptkp  23583  cnmptk1  23584  cnmpt1k  23585  cnmptkk  23586  cnmptk1p  23588  cnmpt2k  23591  qtopeu  23619  pt1hmeo  23709  ptunhmeo  23711  xkocnv  23717  xkohmeo  23718  flfcnp2  23910  cnmpt1plusg  23990  istgp2  23994  tmdmulg  23995  tgpmulg  23996  tmdgsum  23998  subgtgp  24008  symgtgp  24009  tgpconncomp  24016  prdstgpd  24028  tsmsmhm  24049  tsmsadd  24050  tsmssub  24052  tgptsmscls  24053  tsmssplit  24055  tsmsxplem1  24056  tsmsxplem2  24057  cnmpt1vsca  24097  tlmtgp  24099  ustuqtoplem  24143  utopsnneip  24152  ressprdsds  24275  metuval  24453  nmfval0  24494  tngnm  24555  nmoeq0  24640  idnghm  24647  cnmpt1ds  24747  fsumcn  24777  expcn  24779  divccn  24780  expcnOLD  24781  divccnOLD  24782  divccncf  24815  negcncf  24831  negcncfOLD  24832  copco  24934  pcopt  24938  pcopt2  24939  pcoass  24940  pi1xfrcnvlem  24972  cnmpt1ip  25163  rrxnm  25307  rrxds  25309  minveclem3b  25344  divcncf  25364  ovolctb  25407  ovoliunnul  25424  voliunlem3  25469  ovolfs2  25488  uniioombllem2  25500  vitalilem4  25528  vitalilem5  25529  ismbf  25545  mbfss  25563  mbfmulc2re  25565  mbfneg  25567  mbfpos  25568  mbfposb  25570  mbfadd  25578  mbfsub  25579  mbfmulc2  25580  mbfinf  25582  mbflimsup  25583  mbflimlem  25584  i1fpos  25623  i1fposd  25624  itg1climres  25631  mbfmul  25643  itg2mulc  25664  itg2i1fseq  25672  itg2cnlem1  25678  itg2cnlem2  25679  itgresr  25696  iblneg  25720  i1fibl  25725  itgitg1  25726  iblsub  25739  itgfsum  25744  itgmulc2lem1  25749  limcmpt  25800  limccnp  25808  limcco  25810  dvreslem  25826  dvres2lem  25827  dvidlem  25832  dvcnp2  25837  dvcnp2OLD  25838  dvaddbr  25856  dvmulbr  25857  dvmulbrOLD  25858  dvmulf  25862  dvcmulf  25864  dvcobr  25865  dvcobrOLD  25866  dvcof  25868  dvcjbr  25869  dvcj  25870  dvfre  25871  dvexp  25873  dvexp2  25874  dvrec  25875  dvmptcmul  25884  dvmptdivc  25885  dvmptneg  25886  dvmptsub  25887  dvmptre  25889  dvmptim  25890  dvrecg  25893  dvmptdiv  25894  dvmptfsum  25895  dvcnvlem  25896  dvcnv  25897  dvexp3  25898  dvef  25900  dvsincos  25901  dv11cn  25922  lhop2  25936  lhop  25937  ftc2  25967  itgparts  25970  itgsubstlem  25971  mdegfval  25983  mdegmullem  25999  ply1termlem  26124  plypow  26126  plyconst  26127  plyeq0lem  26131  plypf1  26133  plyaddlem1  26134  plymullem1  26135  coeeulem  26145  coeidlem  26158  plyco  26162  coeeq2  26163  0dgr  26166  0dgrb  26167  dgrcolem1  26195  dgrcolem2  26196  plycjlem  26198  dvply1  26207  dvply2g  26208  dvply2gOLD  26209  plydiveu  26222  plyremlem  26228  elqaalem3  26245  taylfval  26282  dvtaylp  26294  taylthlem1  26297  taylthlem2  26298  taylthlem2OLD  26299  ulmshft  26315  mtestbdd  26330  iblulm  26332  itgulm2  26334  pserulm  26347  psercn2  26348  psercn2OLD  26349  pserdvlem2  26354  pserdv  26355  pserdv2  26356  abelthlem1  26357  abelthlem3  26359  advlog  26579  advlogexp  26580  dvcxp1  26665  dvcxp2  26666  dvcncxp1  26668  sqrtcn  26676  loglesqrt  26687  dvatan  26861  atantayl2  26864  atantayl3  26865  leibpi  26868  rlimcnp2  26892  efrlim  26895  efrlimOLD  26896  dfef2  26897  cxp2lim  26903  divsqrtsumlem  26906  lgamgulmlem2  26956  lgamgulm2  26962  lgamcvglem  26966  gamcvg2lem  26985  ftalem7  27005  basellem9  27015  muinv  27119  logfacrlim  27151  logexprlim  27152  dchrmullid  27179  dchrinvcl  27180  lgseisenlem3  27304  lgseisenlem4  27305  chtppilimlem2  27401  chebbnd2  27404  chpchtlim  27406  chpo1ub  27407  rpvmasumlem  27414  dchrmusumlema  27420  dchrvmasumlem1  27422  dchrvmasumiflem2  27429  dchrisum0fno1  27438  rpvmasum2  27439  dchrisum0lema  27441  dchrisum0lem1  27443  dchrisum0lem2a  27444  dchrisum0lem2  27445  dchrisum0  27447  dchrmusumlem  27449  dchrvmasumlem  27450  rpvmasum  27453  rplogsum  27454  logdivsum  27460  mulog2sumlem3  27463  vmalogdivsum2  27465  vmalogdivsum  27466  2vmadivsumlem  27467  logsqvma2  27470  log2sumbnd  27471  selberglem2  27473  selberg3lem1  27484  selberg3  27486  selberg4lem1  27487  selberg4  27488  pntrsumo1  27492  selberg3r  27496  selberg4r  27497  selberg34r  27498  pntrlog2bndlem2  27505  pntrlog2bndlem4  27507  pntrlog2bndlem5  27508  pntrlog2bndlem6  27510  padicabvf  27558  padicabvcxp  27559  mirval  28618  crctcshlem4  29783  clwlknf1oclwwlkn  30046  eucrct2eupth  30207  chscllem4  31602  brafnmul  31913  kbmul  31917  cofmpt2  32591  ofresid  32599  ofoprabco  32621  fmptunsnop  32656  fcobijfs  32679  gsummpt2d  33015  gsummptres  33018  gsummptres2  33019  gsummptfsf1o  33020  gsumfs2d  33021  gsumpart  33023  gsumhashmul  33027  gsumwrd2dccat  33033  fzto1st1  33057  fzto1st  33058  elrgspnlem1  33195  elrgspnlem2  33196  elrgspnlem3  33197  elrgspnlem4  33198  elrgspnsubrunlem1  33200  elrgspnsubrunlem2  33201  qusbas2  33356  qusima  33358  elrspunidl  33378  elrspunsn  33379  rprmdvdsprod  33484  ressply1evls1  33513  evl1deg1  33524  evl1deg2  33525  evl1deg3  33526  gsummoncoe1fzo  33542  lbsdiflsp0  33601  fedgmullem1  33604  fedgmullem2  33605  fldextrspunlsplem  33647  fldextrspunlsp  33648  mdetpmtr1  33792  mdetlap  33801  xrge0mulc1cn  33910  esumval  34015  esumsnf  34033  esumpcvgval  34047  esumcvg  34055  esumcvgsum  34057  esumsup  34058  ofcfeqd2  34070  meascnbl  34188  sitgval  34302  probmeasb  34400  cndprobprob  34408  dstfrvclim1  34448  ballotlemfval  34460  ballotlemsval  34479  ballotlemieq  34487  plymul02  34516  plymulx0  34517  plymulx  34518  signsplypnf  34520  signstfv  34533  signstfvn  34539  signstfvp  34541  itgexpif  34576  logdivsqrle  34620  ptpconn  35208  cvmliftlem6  35265  cvmliftphtlem  35292  cvmlift3lem5  35298  elmrsubrn  35495  msubfval  35499  msubco  35506  divcnvlin  35708  knoppcnlem9  36477  knoppcnlem10  36478  knoppcnlem11  36479  bj-finsumval0  37261  curf  37580  matunitlindflem1  37598  matunitlindflem2  37599  poimirlem3  37605  poimirlem15  37617  poimirlem16  37618  poimirlem17  37619  poimirlem19  37621  poimirlem20  37622  broucube  37636  ovoliunnfl  37644  voliunnfl  37646  volsupnfl  37647  mbfposadd  37649  itg2addnclem  37653  itg2addnclem3  37655  itg2addnc  37656  itgaddnclem2  37661  itgaddnc  37662  iblsubnc  37663  itgsubnc  37664  itgmulc2nclem1  37668  itgmulc2nclem2  37669  itgmulc2nc  37670  itgabsnc  37671  ftc1cnnclem  37673  ftc1anclem3  37677  ftc1anclem5  37679  ftc1anclem6  37680  ftc1anclem8  37682  ftc1anc  37683  ftc2nc  37684  areacirclem1  37690  areacirclem2  37691  areacirclem4  37693  areacirc  37695  upixp  37711  lcmineqlem8  42012  lcmineqlem12  42016  dvrelog2b  42042  dvrelogpow2b  42044  aks4d1p1p6  42049  aks4d1p1p5  42051  aks6d1c1  42092  aks6d1c5lem3  42113  sticksstones12a  42133  sticksstones12  42134  sticksstones19  42141  aks6d1c6lem1  42146  aks6d1c6lem4  42149  aks6d1c7lem3  42158  qsalrel  42216  pwsgprod  42520  rhmcomulpsr  42527  evlsvvval  42539  evlsevl  42547  selvvvval  42561  evlselv  42563  fsuppssindlem1  42567  fsuppssind  42569  mhphf  42573  mzpsubst  42724  mzprename  42725  mzpcompact2lem  42727  eldioph2  42738  rabdiophlem2  42778  mendlmod  43165  mendassa  43166  areaquad  43192  fsovcnvlem  43989  hashnzfzclim  44298  expgrowthi  44309  expgrowth  44311  uzmptshftfval  44322  dvradcnv2  44323  binomcxplemrat  44326  binomcxplemfrat  44327  binomcxplemradcnv  44328  binomcxplemdvbinom  44329  binomcxplemcvg  44330  binomcxplemdvsum  44331  binomcxplemnotnn0  44332  mulc1cncfg  45574  expcnfg  45576  fprodcnlem  45584  clim1fr1  45586  divcnvg  45612  sublimc  45637  reclimc  45638  divlimc  45641  limsupresico  45685  limsuppnfdlem  45686  limsupvaluz  45693  supcnvlimsupmpt  45726  liminfresico  45756  climliminflimsupd  45786  cncfmptssg  45856  negcncfg  45866  cncficcgt0  45873  fprodcncf  45885  fprodsubrecnncnvlem  45892  fprodaddrecnncnvlem  45894  dvsinax  45898  dvasinbx  45905  dvdivf  45907  ioodvbdlimc1lem2  45917  ioodvbdlimc2lem  45919  dvnmptdivc  45923  dvxpaek  45925  dvnxpaek  45927  dvnmul  45928  dvnprodlem2  45932  ibliccsinexp  45936  itgsinexplem1  45939  itgsinexp  45940  iblempty  45950  itgcoscmulx  45954  itgsincmulx  45959  itgioocnicc  45962  iblcncfioo  45963  itgsbtaddcnst  45967  volioofmpt  45979  volicofmpt  45982  stoweidlem4  45989  stirlinglem5  46063  dirkerval  46076  dirkertrigeq  46086  dirkeritg  46087  dirkercncflem2  46089  dirkercncflem4  46091  fourierdlem16  46108  fourierdlem18  46110  fourierdlem21  46113  fourierdlem22  46114  fourierdlem28  46120  fourierdlem39  46131  fourierdlem40  46132  fourierdlem41  46133  fourierdlem53  46144  fourierdlem56  46147  fourierdlem57  46148  fourierdlem60  46151  fourierdlem61  46152  fourierdlem68  46159  fourierdlem73  46164  fourierdlem74  46165  fourierdlem75  46166  fourierdlem76  46167  fourierdlem78  46169  fourierdlem81  46172  fourierdlem82  46173  fourierdlem83  46174  fourierdlem84  46175  fourierdlem85  46176  fourierdlem88  46179  fourierdlem90  46181  fourierdlem92  46183  fourierdlem93  46184  fourierdlem95  46186  fourierdlem97  46188  fourierdlem101  46192  fourierdlem103  46194  fourierdlem104  46195  fourierdlem111  46202  fourierdlem112  46203  sqwvfoura  46213  sqwvfourb  46214  fouriersw  46216  elaa2lem  46218  etransclem4  46223  etransclem17  46236  etransclem18  46237  etransclem32  46251  etransclem46  46265  sge0z  46360  sge0revalmpt  46363  sge0tsms  46365  sge0sup  46376  sge0iunmptlemre  46400  sge0iun  46404  sge0xaddlem2  46419  ismeannd  46452  psmeasurelem  46455  meaiuninclem  46465  meaiininclem  46471  caratheodory  46513  isomenndlem  46515  ovnval  46526  hoicvrrex  46541  ovnlecvr  46543  ovncvrrp  46549  ovn0lem  46550  ovnsubaddlem1  46555  hoidmv1lelem2  46577  hoidmv1le  46579  hoidmvlelem3  46582  ovnhoilem2  46587  ovnhoi  46588  ovnlecvr2  46595  ovncvr2  46596  hspmbllem2  46612  ovolval2lem  46628  ovolval3  46632  ovolval5lem1  46637  ovolval5lem2  46638  ovnovollem1  46641  ovnovollem2  46642  vonioolem1  46665  vonicclem1  46668  vonct  46678  smflim  46762  smfinflem  46802  smflimsuplem5  46809  smfliminflem  46815  cfsetsnfsetfv  47045  fundcmpsurbijinjpreimafv  47395  fundcmpsurinjimaid  47399  fdmdifeqresdif  48330  ply1mulgsumlem2  48376  lincvalsc0  48410  linc0scn0  48412  lincdifsn  48413  lincsum  48418  lincscm  48419  lindslinindimp2lem4  48450  lindslinindsimp2lem5  48451  lincresunit3lem2  48469  1arymaptfo  48632  itcovalpclem1  48659  itcovalpclem2  48660  itcovalt2lem1  48664  itcovalt2lem2  48665  tposcurf1  49288  tposcurf2  49289  diag1  49293  fuco22  49328  fucocolem2  49343  fucocolem3  49344  fucocolem4  49345  fucoco  49346  fucolid  49350  fucorid  49351  postcofval  49353  precofval  49356  precofvalALT  49357  precofval2  49358  fucoppcco  49398  islmd  49654  iscmd  49655  aacllem  49790  amgmwlem  49791