Theorem mpteq2dva 5197

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

Syntax hints:   → wi 4   ∧ wa 400   = wceq 1563   ∈ wcel 2145   ↦ cmpt 5185

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1818  ax-4 1832  ax-5 1933  ax-6 1990  ax-7 2031  ax-8 2147  ax-9 2155  ax-ext 2737

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1803  df-sb 2094  df-clab 2744  df-cleq 2757  df-clel 2840  df-opab 5167  df-mpt 5186

This theorem is referenced by:  mpteq2dv  5198  mpteq2ia  5199  2fvcoidd  7285  offval  7673  offval2  7684  coof  7688  caofinvl  7696  caofcom  7701  caofass  7704  caofdi  7706  caofdir  7707  caonncan  7708  curry1  8087  curry2  8090  mpocurryd  8253  pw2f1olem  9057  mapxpen  9119  xpmapenlem  9120  cantnfp1  9638  cantnflem1d  9645  cantnflem1  9646  cnfcom2lem  9658  dfac12lem1  10115  seqof  14083  seqof2  14084  swrdswrd  14730  repswswrd  14809  repswrevw  14812  revco  14859  ccatco  14860  repsco  14865  ofccat  14994  lo1eq  15607  rlimeq  15608  lo1mul2  15668  o1dif  15669  lo1sub  15670  rlimdiv  15685  caucvgr  15715  sumeq1  15728  fsumrlim  15851  fsumo1  15852  climfsum  15860  geomulcvg  15918  vdwlem8  17036  prmgapprmo  17110  restid2  17471  pwsplusgval  17532  pwsmulrval  17533  pwsvscafval  17536  qusin  17586  xpsaddlem  17615  xpsvsca  17619  catidd  17724  fuclid  18014  fucrid  18015  fucass  18016  setcepi  18133  prf1st  18248  prf2nd  18249  1st2ndprf  18250  curfcl  18276  curfuncf  18282  diag2  18289  curf2ndf  18291  hof2val  18300  hofcllem  18302  hofcl  18303  yonedalem4a  18319  yonedalem4c  18321  yonedalem3b  18323  yonedainv  18325  yonffthlem  18326  prdssgrpd  18779  prdsidlem  18815  prdsmndd  18816  mhmvlin  18847  pwsco2mhm  18880  frmdup3lem  18913  frmdup3  18914  smndex1gid  18951  smndex1gidOLD  18952  smndex1igidOLD  18954  grpinvpropd  19069  prdsinvlem  19103  pwsinvg  19107  pwssub  19108  galactghm  19462  cayleylem1  19470  pmtrprfval  19545  sylow1lem2  19657  sylow3lem1  19685  efginvrel1  19786  frgpup3lem  19835  frgpup3  19836  prdscmnd  19919  iscyggen  19938  gsumval3  19965  gsumcllem  19966  gsumzsplit  19985  gsumsub  20006  gsummptf1o  20021  gsum2d  20030  gsum2d2  20032  gsumxp  20034  prdsgsum  20039  telgsumfz  20048  telgsumfz0  20050  telgsum  20052  dprdfsub  20081  dprdfeq0  20082  dprddisj2  20099  dprd2d2  20104  dpjidcl  20118  ablfaclem2  20146  ablfac2  20149  prdsmgp  20215  prdsrngd  20242  srgbinomlem3  20298  srgbinomlem4  20299  srgbinomlem  20300  gsumdixp  20388  prdsringd  20390  pwsgprod  20399  prdslmodd  21056  mulgrhm2  21585  frgpcyg  21680  freshmansdream  21681  evpmodpmf1o  21703  phlpropd  21762  frlmphl  21888  uvcresum  21900  frlmup1  21905  asclpropd  22004  psrass1lem  22040  psrlinv  22062  psrass1  22070  psrdi  22071  psrdir  22072  psrass23l  22073  psrcom  22074  psrass23  22075  resspsrmul  22082  mplsubrglem  22110  mplmonmul  22144  mplcoe1  22145  mplcoe5  22148  mplcoe4  22179  evlslem3  22188  evlslem1  22190  evlsvvval  22201  rhmcomulmpl  22232  evlsevl  22240  selvvvval  22250  mhpmulcl  22269  psdmplcl  22282  psdadd  22283  psdmul  22286  psdmvr  22289  psrplusgpropd  22352  psropprmul  22354  coe1mul2  22387  coe1tm  22391  coe1tmmul2  22394  coe1tmmul  22395  coe1pwmul  22397  cply1mul  22413  ply1coe  22415  eqcoe1ply1eq  22416  lply1binomsc  22428  evl1gsummon  22482  evls1fpws  22486  mamures  22511  grpvrinv  22513  mamuass  22516  mamudi  22517  mamudir  22518  mamuvs1  22519  mamuvs2  22520  mpomatmul  22560  mamutpos  22572  madetsumid  22575  dmatmul  22611  scmatscm  22627  1mavmul  22662  mavmulass  22663  mvmumamul1  22668  mulmarep1gsum1  22687  mulmarep1gsum2  22688  mdetleib2  22702  mdetfval1  22704  mdet0pr  22706  mdetdiag  22713  mdetdiagid  22714  mdetrlin  22716  mdetrsca  22717  mdetralt  22722  mdetunilem9  22734  gsummatr01  22773  smadiadetlem1a  22777  smadiadetlem3  22782  smadiadetlem4  22783  cpmatmcllem  22832  mat2pmatmul  22845  decpmatmullem  22885  decpmatmul  22886  pmatcollpw1lem2  22889  pmatcollpw  22895  pmatcollpw3lem  22897  pmatcollpwscmat  22905  idpm2idmp  22915  mp2pm2mplem3  22922  mp2pm2mplem4  22923  mp2pm2mplem5  22924  mp2pm2mp  22925  pm2mpghm  22930  pm2mpmhmlem2  22933  monmat2matmon  22938  pm2mp  22939  chpdmat  22955  chpscmat  22956  chpscmatgsumbin  22958  chpscmatgsummon  22959  chp0mat  22960  chpidmat  22961  chfacfscmulgsum  22974  chfacfpmmulgsum  22978  chfacfpmmulgsum2  22979  cayhamlem1  22980  cpmidgsumm2pm  22983  cpmidpmat  22987  cpmadugsumlemB  22988  cpmadugsumlemC  22989  cpmadugsumlemF  22990  cpmadumatpoly  22997  cayhamlem3  23001  cayhamlem4  23002  cayleyhamilton0  23003  cayleyhamiltonALT  23005  neiptopnei  23246  neiptopreu  23247  ptcnplem  23735  cnmpt1t  23779  cnmpt12  23781  cnmptkp  23794  cnmptk1  23795  cnmpt1k  23796  cnmptkk  23797  cnmptk1p  23799  cnmpt2k  23802  qtopeu  23830  pt1hmeo  23920  ptunhmeo  23922  xkocnv  23928  xkohmeo  23929  flfcnp2  24121  cnmpt1plusg  24201  istgp2  24205  tmdmulg  24206  tgpmulg  24207  tmdgsum  24209  subgtgp  24219  symgtgp  24220  tgpconncomp  24227  prdstgpd  24239  tsmsmhm  24260  tsmsadd  24261  tsmssub  24263  tgptsmscls  24264  tsmssplit  24266  tsmsxplem1  24267  tsmsxplem2  24268  cnmpt1vsca  24308  tlmtgp  24310  ustuqtoplem  24353  utopsnneip  24362  ressprdsds  24485  metuval  24663  nmfval0  24704  tngnm  24765  nmoeq0  24850  idnghm  24857  cnmpt1ds  24957  fsumcn  24986  expcn  24988  divccn  24989  divccncf  25022  negcncf  25038  copco  25134  pcopt  25138  pcopt2  25139  pcoass  25140  pi1xfrcnvlem  25172  cnmpt1ip  25363  rrxnm  25507  rrxds  25509  minveclem3b  25544  divcncf  25563  ovolctb  25606  ovoliunnul  25623  voliunlem3  25668  ovolfs2  25687  uniioombllem2  25699  vitalilem4  25727  vitalilem5  25728  ismbf  25744  mbfss  25762  mbfmulc2re  25764  mbfneg  25766  mbfpos  25767  mbfposb  25769  mbfadd  25777  mbfsub  25778  mbfmulc2  25779  mbfinf  25781  mbflimsup  25782  mbflimlem  25783  i1fpos  25822  i1fposd  25823  itg1climres  25830  mbfmul  25842  itg2mulc  25863  itg2i1fseq  25871  itg2cnlem1  25877  itg2cnlem2  25878  itgresr  25895  iblneg  25919  i1fibl  25924  itgitg1  25925  iblsub  25938  itgfsum  25943  itgmulc2lem1  25948  limcmpt  25999  limccnp  26007  limcco  26009  dvreslem  26025  dvres2lem  26026  dvidlem  26031  dvcnp2  26036  dvaddbr  26054  dvmulbr  26055  dvmulf  26059  dvcmulf  26061  dvcobr  26062  dvcof  26064  dvcjbr  26065  dvcj  26066  dvfre  26067  dvexp  26069  dvexp2  26070  dvrec  26071  dvmptcmul  26080  dvmptdivc  26081  dvmptneg  26082  dvmptsub  26083  dvmptre  26085  dvmptim  26086  dvrecg  26089  dvmptdiv  26090  dvmptfsum  26091  dvcnvlem  26092  dvcnv  26093  dvexp3  26094  dvef  26096  dvsincos  26097  dv11cn  26117  lhop2  26131  lhop  26132  ftc2  26160  itgparts  26163  itgsubstlem  26164  mdegfval  26176  mdegmullem  26192  ply1termlem  26317  plypow  26319  plyconst  26320  plyeq0lem  26324  plypf1  26326  plyaddlem1  26327  plymullem1  26328  coeeulem  26338  coeidlem  26351  plyco  26355  coeeq2  26356  0dgr  26359  0dgrb  26360  dgrcolem1  26387  dgrcolem2  26388  plycjlem  26390  plymul02  26398  plyn0mulidp  26399  plymulidp  26400  dvply1  26402  dvply2g  26403  plydiveu  26416  plyremlem  26422  elqaalem3  26439  taylfval  26476  dvtaylp  26487  taylthlem1  26490  taylthlem2  26491  ulmshft  26507  mtestbdd  26522  iblulm  26524  itgulm2  26526  pserulm  26539  psercn2  26540  pserdvlem2  26545  pserdv  26546  pserdv2  26547  abelthlem1  26548  abelthlem3  26550  advlog  26773  advlogexp  26774  dvcxp1  26859  dvcxp2  26860  dvcncxp1  26862  sqrtcn  26869  loglesqrt  26880  dvatan  27054  atantayl2  27057  atantayl3  27058  leibpi  27061  rlimcnp2  27085  efrlim  27088  dfef2  27089  cxp2lim  27095  divsqrtsumlem  27098  lgamgulmlem2  27148  lgamgulm2  27154  lgamcvglem  27158  gamcvg2lem  27177  ftalem7  27197  basellem9  27207  muinv  27311  logfacrlim  27342  logexprlim  27343  dchrmullid  27370  dchrinvcl  27371  lgseisenlem3  27495  lgseisenlem4  27496  chtppilimlem2  27592  chebbnd2  27595  chpchtlim  27597  chpo1ub  27598  rpvmasumlem  27605  dchrmusumlema  27611  dchrvmasumlem1  27613  dchrvmasumiflem2  27620  dchrisum0fno1  27629  rpvmasum2  27630  dchrisum0lema  27632  dchrisum0lem1  27634  dchrisum0lem2a  27635  dchrisum0lem2  27636  dchrisum0  27638  dchrmusumlem  27640  dchrvmasumlem  27641  rpvmasum  27644  rplogsum  27645  logdivsum  27651  mulog2sumlem3  27654  vmalogdivsum2  27656  vmalogdivsum  27657  2vmadivsumlem  27658  logsqvma2  27661  log2sumbnd  27662  selberglem2  27664  selberg3lem1  27675  selberg3  27677  selberg4lem1  27678  selberg4  27679  pntrsumo1  27683  selberg3r  27687  selberg4r  27688  selberg34r  27689  pntrlog2bndlem2  27696  pntrlog2bndlem4  27698  pntrlog2bndlem5  27699  pntrlog2bndlem6  27701  padicabvf  27749  padicabvcxp  27750  mirval  28882  crctcshlem4  30074  clwlknf1oclwwlkn  30340  eucrct2eupth  30501  chscllem4  31897  brafnmul  32208  kbmul  32212  cofmpt2  32887  ofresid  32895  ofoprabco  32917  fmptunsnop  32953  fcobijfs  32974  fcobijfs2  32975  gsummpt2d  33277  gsummptres  33280  gsummptres2  33281  gsummptf1od  33283  gsummptp1  33285  gsummptfsf1o  33288  gsumfs2d  33289  gsumpart  33291  gsumhashmul  33295  gsummulsubdishift1  33296  gsummulsubdishift2  33297  gsumwrd2dccat  33306  fzto1st1  33330  fzto1st  33331  elrgspnlem1  33470  elrgspnlem2  33471  elrgspnlem3  33472  elrgspnlem4  33473  elrgspnsubrunlem1  33475  elrgspnsubrunlem2  33476  qusbas2  33626  qusima  33628  elrspunidl  33647  elrspunsn  33648  rprmdvdsprod  33736  ressply1evls1  33767  evl1deg1  33778  evl1deg2  33779  evl1deg3  33780  gsummoncoe1fzo  33799  mplasclco  33818  selvply1rhmlemb  33821  selvply1rhmlem2  33823  selvply1rhmlem4  33825  selvply1rhm0  33828  mplmulmvr  33841  evlextv  33844  mplvrpmga  33847  mplvrpmmhm  33848  mplvrpmrhm  33849  psrgsum  33850  psrmonmul  33852  issply  33863  esplyfval0  33866  esplyfval3  33874  esplyfval1  33875  esplyfvaln  33876  esplyind  33877  vietalem  33881  lbsdiflsp0  33928  fedgmullem1  33931  fedgmullem2  33932  fldextrspunlsplem  33975  fldextrspunlsp  33976  extdgfialglem2  33995  mdetpmtr1  34125  mdetlap  34134  xrge0mulc1cn  34243  esumval  34348  esumsnf  34366  esumpcvgval  34380  esumcvg  34388  esumcvgsum  34390  esumsup  34391  ofcfeqd2  34403  meascnbl  34521  sitgval  34634  probmeasb  34732  cndprobprob  34740  dstfrvclim1  34780  ballotlemfval  34792  ballotlemsval  34811  ballotlemieq  34819  signsplypnf  34849  signstfv  34862  signstfvn  34868  signstfvp  34870  itgexpif  34905  logdivsqrle  34949  ptpconn  35591  cvmliftlem6  35648  cvmliftphtlem  35675  cvmlift3lem5  35681  elmrsubrn  35878  msubfval  35882  msubco  35889  divcnvlin  36091  knoppcnlem9  36947  knoppcnlem10  36948  knoppcnlem11  36949  bj-finsumval0  37784  curf  38104  matunitlindflem1  38122  matunitlindflem2  38123  poimirlem3  38129  poimirlem15  38141  poimirlem16  38142  poimirlem17  38143  poimirlem19  38145  poimirlem20  38146  broucube  38160  ovoliunnfl  38168  voliunnfl  38170  volsupnfl  38171  mbfposadd  38173  itg2addnclem  38177  itg2addnclem3  38179  itg2addnc  38180  itgaddnclem2  38185  itgaddnc  38186  iblsubnc  38187  itgsubnc  38188  itgmulc2nclem1  38192  itgmulc2nclem2  38193  itgmulc2nc  38194  itgabsnc  38195  ftc1cnnclem  38197  ftc1anclem3  38201  ftc1anclem5  38203  ftc1anclem6  38204  ftc1anclem8  38206  ftc1anc  38207  ftc2nc  38208  areacirclem1  38214  areacirclem2  38215  areacirclem4  38217  areacirc  38219  upixp  38235  lcmineqlem8  42660  lcmineqlem12  42664  dvrelog2b  42690  dvrelogpow2b  42692  aks4d1p1p6  42697  aks4d1p1p5  42699  aks6d1c1  42740  aks6d1c5lem3  42761  sticksstones12a  42781  sticksstones12  42782  sticksstones19  42789  aks6d1c6lem1  42794  aks6d1c6lem4  42797  aks6d1c7lem3  42806  qsalrel  42864  rhmcomulpsr  43171  evlselv  43178  fsuppssindlem1  43180  fsuppssind  43182  mhphf  43186  mzpsubst  43336  mzprename  43337  mzpcompact2lem  43339  eldioph2  43350  rabdiophlem2  43386  mendlmod  43773  mendassa  43774  areaquad  43800  fsovcnvlem  44596  hashnzfzclim  44891  expgrowthi  44902  expgrowth  44904  uzmptshftfval  44915  dvradcnv2  44916  binomcxplemrat  44919  binomcxplemfrat  44920  binomcxplemradcnv  44921  binomcxplemdvbinom  44922  binomcxplemcvg  44923  binomcxplemdvsum  44924  binomcxplemnotnn0  44925  mulc1cncfg  46164  expcnfg  46166  fprodcnlem  46174  clim1fr1  46176  divcnvg  46202  sublimc  46225  reclimc  46226  divlimc  46229  limsupresico  46273  limsuppnfdlem  46274  limsupvaluz  46281  supcnvlimsupmpt  46314  liminfresico  46344  climliminflimsupd  46374  cncfmptssg  46444  negcncfg  46454  cncficcgt0  46461  fprodcncf  46473  fprodsubrecnncnvlem  46480  fprodaddrecnncnvlem  46482  dvsinax  46486  dvasinbx  46493  dvdivf  46495  ioodvbdlimc1lem2  46505  ioodvbdlimc2lem  46507  dvnmptdivc  46511  dvxpaek  46513  dvnxpaek  46515  dvnmul  46516  dvnprodlem2  46520  ibliccsinexp  46524  itgsinexplem1  46527  itgsinexp  46528  iblempty  46538  itgcoscmulx  46542  itgsincmulx  46547  itgioocnicc  46550  iblcncfioo  46551  itgsbtaddcnst  46555  volioofmpt  46567  volicofmpt  46570  stoweidlem4  46577  stirlinglem5  46651  dirkerval  46664  dirkertrigeq  46674  dirkeritg  46675  dirkercncflem2  46677  dirkercncflem4  46679  fourierdlem16  46696  fourierdlem18  46698  fourierdlem21  46701  fourierdlem22  46702  fourierdlem28  46708  fourierdlem39  46719  fourierdlem40  46720  fourierdlem41  46721  fourierdlem53  46732  fourierdlem56  46735  fourierdlem57  46736  fourierdlem60  46739  fourierdlem61  46740  fourierdlem68  46747  fourierdlem73  46752  fourierdlem74  46753  fourierdlem75  46754  fourierdlem76  46755  fourierdlem78  46757  fourierdlem81  46760  fourierdlem82  46761  fourierdlem83  46762  fourierdlem84  46763  fourierdlem85  46764  fourierdlem88  46767  fourierdlem90  46769  fourierdlem92  46771  fourierdlem93  46772  fourierdlem95  46774  fourierdlem97  46776  fourierdlem101  46780  fourierdlem103  46782  fourierdlem104  46783  fourierdlem111  46790  fourierdlem112  46791  sqwvfoura  46801  sqwvfourb  46802  fouriersw  46804  elaa2lem  46806  etransclem4  46811  etransclem17  46824  etransclem18  46825  etransclem32  46839  etransclem46  46853  sge0z  46948  sge0revalmpt  46951  sge0tsms  46953  sge0sup  46964  sge0iunmptlemre  46988  sge0iun  46992  sge0xaddlem2  47007  ismeannd  47040  psmeasurelem  47043  meaiuninclem  47053  meaiininclem  47059  caratheodory  47101  isomenndlem  47103  ovnval  47114  hoicvrrex  47129  ovnlecvr  47131  ovncvrrp  47137  ovn0lem  47138  ovnsubaddlem1  47143  hoidmv1lelem2  47165  hoidmv1le  47167  hoidmvlelem3  47170  ovnhoilem2  47175  ovnhoi  47176  ovnlecvr2  47183  ovncvr2  47184  hspmbllem2  47200  ovolval2lem  47216  ovolval3  47220  ovolval5lem1  47225  ovolval5lem2  47226  ovnovollem1  47229  ovnovollem2  47230  vonioolem1  47253  vonicclem1  47256  vonct  47266  smflim  47350  smfinflem  47390  smflimsuplem5  47397  smfliminflem  47403  cfsetsnfsetfv  47650  fundcmpsurbijinjpreimafv  48012  fundcmpsurinjimaid  48016  fdmdifeqresdif  48974  ply1mulgsumlem2  49019  lincvalsc0  49053  linc0scn0  49055  lincdifsn  49056  lincsum  49061  lincscm  49062  lindslinindimp2lem4  49093  lindslinindsimp2lem5  49094  lincresunit3lem2  49112  1arymaptfo  49275  itcovalpclem1  49302  itcovalpclem2  49303  itcovalt2lem1  49307  itcovalt2lem2  49308  tposcurf1  49929  tposcurf2  49930  diag1  49934  fuco22  49969  fucocolem2  49984  fucocolem3  49985  fucocolem4  49986  fucoco  49987  fucolid  49991  fucorid  49992  postcofval  49994  precofval  49997  precofvalALT  49998  precofval2  49999  fucoppcco  50039  islmd  50295  iscmd  50296  aacllem  50431  amgmwlem  50432