Theorem mpteq2dva 5191

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

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1541   ∈ wcel 2113   ↦ cmpt 5179

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-sb 2068  df-clab 2715  df-cleq 2728  df-clel 2811  df-opab 5161  df-mpt 5180

This theorem is referenced by:  mpteq2dv  5192  mpteq2ia  5193  2fvcoidd  7243  offval  7631  offval2  7642  coof  7646  caofinvl  7654  caofcom  7659  caofass  7662  caofdi  7664  caofdir  7665  caonncan  7666  curry1  8046  curry2  8049  mpocurryd  8211  pw2f1olem  9009  mapxpen  9071  xpmapenlem  9072  cantnfp1  9590  cantnflem1d  9597  cantnflem1  9598  cnfcom2lem  9610  dfac12lem1  10054  seqof  13982  seqof2  13983  swrdswrd  14628  repswswrd  14707  repswrevw  14710  revco  14757  ccatco  14758  repsco  14763  ofccat  14892  lo1eq  15491  rlimeq  15492  lo1mul2  15552  o1dif  15553  lo1sub  15554  rlimdiv  15569  caucvgr  15599  sumeq1  15612  fsumrlim  15734  fsumo1  15735  climfsum  15743  geomulcvg  15799  vdwlem8  16916  prmgapprmo  16990  restid2  17350  pwsplusgval  17411  pwsmulrval  17412  pwsvscafval  17415  qusin  17465  xpsaddlem  17494  xpsvsca  17498  catidd  17603  fuclid  17893  fucrid  17894  fucass  17895  setcepi  18012  prf1st  18127  prf2nd  18128  1st2ndprf  18129  curfcl  18155  curfuncf  18161  diag2  18168  curf2ndf  18170  hof2val  18179  hofcllem  18181  hofcl  18182  yonedalem4a  18198  yonedalem4c  18200  yonedalem3b  18202  yonedainv  18204  yonffthlem  18205  prdssgrpd  18658  prdsidlem  18694  prdsmndd  18695  mhmvlin  18726  pwsco2mhm  18758  frmdup3lem  18791  frmdup3  18792  smndex1gid  18828  smndex1igid  18829  grpinvpropd  18945  prdsinvlem  18979  pwsinvg  18983  pwssub  18984  galactghm  19333  cayleylem1  19341  pmtrprfval  19416  sylow1lem2  19528  sylow3lem1  19556  efginvrel1  19657  frgpup3lem  19706  frgpup3  19707  prdscmnd  19790  iscyggen  19809  gsumval3  19836  gsumcllem  19837  gsumzsplit  19856  gsumsub  19877  gsummptf1o  19892  gsum2d  19901  gsum2d2  19903  gsumxp  19905  prdsgsum  19910  telgsumfz  19919  telgsumfz0  19921  telgsum  19923  dprdfsub  19952  dprdfeq0  19953  dprddisj2  19970  dprd2d2  19975  dpjidcl  19989  ablfaclem2  20017  ablfac2  20020  prdsmgp  20086  prdsrngd  20111  srgbinomlem3  20163  srgbinomlem4  20164  srgbinomlem  20165  gsumdixp  20254  prdsringd  20256  pwsgprod  20265  prdslmodd  20920  mulgrhm2  21433  frgpcyg  21528  freshmansdream  21529  evpmodpmf1o  21551  phlpropd  21610  frlmphl  21736  uvcresum  21748  frlmup1  21753  asclpropd  21853  psrass1lem  21888  psrlinv  21911  psrass1  21919  psrdi  21920  psrdir  21921  psrass23l  21922  psrcom  21923  psrass23  21924  resspsrmul  21931  mplsubrglem  21959  mplmonmul  21991  mplcoe1  21992  mplcoe5  21995  mplcoe4  22026  evlslem3  22035  evlslem1  22037  evlsvvval  22048  mhpmulcl  22092  psdmplcl  22105  psdadd  22106  psdmul  22109  psdmvr  22112  psrplusgpropd  22176  psropprmul  22178  coe1mul2  22211  coe1tm  22215  coe1tmmul2  22218  coe1tmmul  22219  coe1pwmul  22221  cply1mul  22240  ply1coe  22242  eqcoe1ply1eq  22243  lply1binomsc  22255  evl1gsummon  22309  evls1fpws  22313  rhmcomulmpl  22326  mamures  22341  grpvrinv  22343  mamuass  22346  mamudi  22347  mamudir  22348  mamuvs1  22349  mamuvs2  22350  mpomatmul  22390  mamutpos  22402  madetsumid  22405  dmatmul  22441  scmatscm  22457  1mavmul  22492  mavmulass  22493  mvmumamul1  22498  mulmarep1gsum1  22517  mulmarep1gsum2  22518  mdetleib2  22532  mdetfval1  22534  mdet0pr  22536  mdetdiag  22543  mdetdiagid  22544  mdetrlin  22546  mdetrsca  22547  mdetralt  22552  mdetunilem9  22564  gsummatr01  22603  smadiadetlem1a  22607  smadiadetlem3  22612  smadiadetlem4  22613  cpmatmcllem  22662  mat2pmatmul  22675  decpmatmullem  22715  decpmatmul  22716  pmatcollpw1lem2  22719  pmatcollpw  22725  pmatcollpw3lem  22727  pmatcollpwscmat  22735  idpm2idmp  22745  mp2pm2mplem3  22752  mp2pm2mplem4  22753  mp2pm2mplem5  22754  mp2pm2mp  22755  pm2mpghm  22760  pm2mpmhmlem2  22763  monmat2matmon  22768  pm2mp  22769  chpdmat  22785  chpscmat  22786  chpscmatgsumbin  22788  chpscmatgsummon  22789  chp0mat  22790  chpidmat  22791  chfacfscmulgsum  22804  chfacfpmmulgsum  22808  chfacfpmmulgsum2  22809  cayhamlem1  22810  cpmidgsumm2pm  22813  cpmidpmat  22817  cpmadugsumlemB  22818  cpmadugsumlemC  22819  cpmadugsumlemF  22820  cpmadumatpoly  22827  cayhamlem3  22831  cayhamlem4  22832  cayleyhamilton0  22833  cayleyhamiltonALT  22835  neiptopnei  23076  neiptopreu  23077  ptcnplem  23565  cnmpt1t  23609  cnmpt12  23611  cnmptkp  23624  cnmptk1  23625  cnmpt1k  23626  cnmptkk  23627  cnmptk1p  23629  cnmpt2k  23632  qtopeu  23660  pt1hmeo  23750  ptunhmeo  23752  xkocnv  23758  xkohmeo  23759  flfcnp2  23951  cnmpt1plusg  24031  istgp2  24035  tmdmulg  24036  tgpmulg  24037  tmdgsum  24039  subgtgp  24049  symgtgp  24050  tgpconncomp  24057  prdstgpd  24069  tsmsmhm  24090  tsmsadd  24091  tsmssub  24093  tgptsmscls  24094  tsmssplit  24096  tsmsxplem1  24097  tsmsxplem2  24098  cnmpt1vsca  24138  tlmtgp  24140  ustuqtoplem  24183  utopsnneip  24192  ressprdsds  24315  metuval  24493  nmfval0  24534  tngnm  24595  nmoeq0  24680  idnghm  24687  cnmpt1ds  24787  fsumcn  24817  expcn  24819  divccn  24820  expcnOLD  24821  divccnOLD  24822  divccncf  24855  negcncf  24871  negcncfOLD  24872  copco  24974  pcopt  24978  pcopt2  24979  pcoass  24980  pi1xfrcnvlem  25012  cnmpt1ip  25203  rrxnm  25347  rrxds  25349  minveclem3b  25384  divcncf  25404  ovolctb  25447  ovoliunnul  25464  voliunlem3  25509  ovolfs2  25528  uniioombllem2  25540  vitalilem4  25568  vitalilem5  25569  ismbf  25585  mbfss  25603  mbfmulc2re  25605  mbfneg  25607  mbfpos  25608  mbfposb  25610  mbfadd  25618  mbfsub  25619  mbfmulc2  25620  mbfinf  25622  mbflimsup  25623  mbflimlem  25624  i1fpos  25663  i1fposd  25664  itg1climres  25671  mbfmul  25683  itg2mulc  25704  itg2i1fseq  25712  itg2cnlem1  25718  itg2cnlem2  25719  itgresr  25736  iblneg  25760  i1fibl  25765  itgitg1  25766  iblsub  25779  itgfsum  25784  itgmulc2lem1  25789  limcmpt  25840  limccnp  25848  limcco  25850  dvreslem  25866  dvres2lem  25867  dvidlem  25872  dvcnp2  25877  dvcnp2OLD  25878  dvaddbr  25896  dvmulbr  25897  dvmulbrOLD  25898  dvmulf  25902  dvcmulf  25904  dvcobr  25905  dvcobrOLD  25906  dvcof  25908  dvcjbr  25909  dvcj  25910  dvfre  25911  dvexp  25913  dvexp2  25914  dvrec  25915  dvmptcmul  25924  dvmptdivc  25925  dvmptneg  25926  dvmptsub  25927  dvmptre  25929  dvmptim  25930  dvrecg  25933  dvmptdiv  25934  dvmptfsum  25935  dvcnvlem  25936  dvcnv  25937  dvexp3  25938  dvef  25940  dvsincos  25941  dv11cn  25962  lhop2  25976  lhop  25977  ftc2  26007  itgparts  26010  itgsubstlem  26011  mdegfval  26023  mdegmullem  26039  ply1termlem  26164  plypow  26166  plyconst  26167  plyeq0lem  26171  plypf1  26173  plyaddlem1  26174  plymullem1  26175  coeeulem  26185  coeidlem  26198  plyco  26202  coeeq2  26203  0dgr  26206  0dgrb  26207  dgrcolem1  26235  dgrcolem2  26236  plycjlem  26238  dvply1  26247  dvply2g  26248  dvply2gOLD  26249  plydiveu  26262  plyremlem  26268  elqaalem3  26285  taylfval  26322  dvtaylp  26334  taylthlem1  26337  taylthlem2  26338  taylthlem2OLD  26339  ulmshft  26355  mtestbdd  26370  iblulm  26372  itgulm2  26374  pserulm  26387  psercn2  26388  psercn2OLD  26389  pserdvlem2  26394  pserdv  26395  pserdv2  26396  abelthlem1  26397  abelthlem3  26399  advlog  26619  advlogexp  26620  dvcxp1  26705  dvcxp2  26706  dvcncxp1  26708  sqrtcn  26716  loglesqrt  26727  dvatan  26901  atantayl2  26904  atantayl3  26905  leibpi  26908  rlimcnp2  26932  efrlim  26935  efrlimOLD  26936  dfef2  26937  cxp2lim  26943  divsqrtsumlem  26946  lgamgulmlem2  26996  lgamgulm2  27002  lgamcvglem  27006  gamcvg2lem  27025  ftalem7  27045  basellem9  27055  muinv  27159  logfacrlim  27191  logexprlim  27192  dchrmullid  27219  dchrinvcl  27220  lgseisenlem3  27344  lgseisenlem4  27345  chtppilimlem2  27441  chebbnd2  27444  chpchtlim  27446  chpo1ub  27447  rpvmasumlem  27454  dchrmusumlema  27460  dchrvmasumlem1  27462  dchrvmasumiflem2  27469  dchrisum0fno1  27478  rpvmasum2  27479  dchrisum0lema  27481  dchrisum0lem1  27483  dchrisum0lem2a  27484  dchrisum0lem2  27485  dchrisum0  27487  dchrmusumlem  27489  dchrvmasumlem  27490  rpvmasum  27493  rplogsum  27494  logdivsum  27500  mulog2sumlem3  27503  vmalogdivsum2  27505  vmalogdivsum  27506  2vmadivsumlem  27507  logsqvma2  27510  log2sumbnd  27511  selberglem2  27513  selberg3lem1  27524  selberg3  27526  selberg4lem1  27527  selberg4  27528  pntrsumo1  27532  selberg3r  27536  selberg4r  27537  selberg34r  27538  pntrlog2bndlem2  27545  pntrlog2bndlem4  27547  pntrlog2bndlem5  27548  pntrlog2bndlem6  27550  padicabvf  27598  padicabvcxp  27599  mirval  28727  crctcshlem4  29893  clwlknf1oclwwlkn  30159  eucrct2eupth  30320  chscllem4  31715  brafnmul  32026  kbmul  32030  cofmpt2  32712  ofresid  32720  ofoprabco  32742  fmptunsnop  32779  fcobijfs  32800  fcobijfs2  32801  gsummpt2d  33132  gsummptres  33135  gsummptres2  33136  gsummptf1od  33138  gsummptp1  33140  gsummptfsf1o  33143  gsumfs2d  33144  gsumpart  33146  gsumhashmul  33150  gsummulsubdishift1  33151  gsummulsubdishift2  33152  gsumwrd2dccat  33160  fzto1st1  33184  fzto1st  33185  elrgspnlem1  33324  elrgspnlem2  33325  elrgspnlem3  33326  elrgspnlem4  33327  elrgspnsubrunlem1  33329  elrgspnsubrunlem2  33330  qusbas2  33487  qusima  33489  elrspunidl  33509  elrspunsn  33510  rprmdvdsprod  33615  ressply1evls1  33646  evl1deg1  33657  evl1deg2  33658  evl1deg3  33659  gsummoncoe1fzo  33678  mplmulmvr  33704  evlextv  33707  mplvrpmga  33710  mplvrpmmhm  33711  mplvrpmrhm  33712  issply  33719  esplyfval0  33722  esplyfval3  33730  esplyind  33731  vietalem  33735  lbsdiflsp0  33783  fedgmullem1  33786  fedgmullem2  33787  fldextrspunlsplem  33830  fldextrspunlsp  33831  extdgfialglem2  33850  mdetpmtr1  33980  mdetlap  33989  xrge0mulc1cn  34098  esumval  34203  esumsnf  34221  esumpcvgval  34235  esumcvg  34243  esumcvgsum  34245  esumsup  34246  ofcfeqd2  34258  meascnbl  34376  sitgval  34489  probmeasb  34587  cndprobprob  34595  dstfrvclim1  34635  ballotlemfval  34647  ballotlemsval  34666  ballotlemieq  34674  plymul02  34703  plymulx0  34704  plymulx  34705  signsplypnf  34707  signstfv  34720  signstfvn  34726  signstfvp  34728  itgexpif  34763  logdivsqrle  34807  ptpconn  35427  cvmliftlem6  35484  cvmliftphtlem  35511  cvmlift3lem5  35517  elmrsubrn  35714  msubfval  35718  msubco  35725  divcnvlin  35927  knoppcnlem9  36701  knoppcnlem10  36702  knoppcnlem11  36703  bj-finsumval0  37490  curf  37799  matunitlindflem1  37817  matunitlindflem2  37818  poimirlem3  37824  poimirlem15  37836  poimirlem16  37837  poimirlem17  37838  poimirlem19  37840  poimirlem20  37841  broucube  37855  ovoliunnfl  37863  voliunnfl  37865  volsupnfl  37866  mbfposadd  37868  itg2addnclem  37872  itg2addnclem3  37874  itg2addnc  37875  itgaddnclem2  37880  itgaddnc  37881  iblsubnc  37882  itgsubnc  37883  itgmulc2nclem1  37887  itgmulc2nclem2  37888  itgmulc2nc  37889  itgabsnc  37890  ftc1cnnclem  37892  ftc1anclem3  37896  ftc1anclem5  37898  ftc1anclem6  37899  ftc1anclem8  37901  ftc1anc  37902  ftc2nc  37903  areacirclem1  37909  areacirclem2  37910  areacirclem4  37912  areacirc  37914  upixp  37930  lcmineqlem8  42290  lcmineqlem12  42294  dvrelog2b  42320  dvrelogpow2b  42322  aks4d1p1p6  42327  aks4d1p1p5  42329  aks6d1c1  42370  aks6d1c5lem3  42391  sticksstones12a  42411  sticksstones12  42412  sticksstones19  42419  aks6d1c6lem1  42424  aks6d1c6lem4  42427  aks6d1c7lem3  42436  qsalrel  42496  rhmcomulpsr  42804  evlsevl  42817  selvvvval  42828  evlselv  42830  fsuppssindlem1  42834  fsuppssind  42836  mhphf  42840  mzpsubst  42990  mzprename  42991  mzpcompact2lem  42993  eldioph2  43004  rabdiophlem2  43044  mendlmod  43431  mendassa  43432  areaquad  43458  fsovcnvlem  44254  hashnzfzclim  44563  expgrowthi  44574  expgrowth  44576  uzmptshftfval  44587  dvradcnv2  44588  binomcxplemrat  44591  binomcxplemfrat  44592  binomcxplemradcnv  44593  binomcxplemdvbinom  44594  binomcxplemcvg  44595  binomcxplemdvsum  44596  binomcxplemnotnn0  44597  mulc1cncfg  45835  expcnfg  45837  fprodcnlem  45845  clim1fr1  45847  divcnvg  45873  sublimc  45896  reclimc  45897  divlimc  45900  limsupresico  45944  limsuppnfdlem  45945  limsupvaluz  45952  supcnvlimsupmpt  45985  liminfresico  46015  climliminflimsupd  46045  cncfmptssg  46115  negcncfg  46125  cncficcgt0  46132  fprodcncf  46144  fprodsubrecnncnvlem  46151  fprodaddrecnncnvlem  46153  dvsinax  46157  dvasinbx  46164  dvdivf  46166  ioodvbdlimc1lem2  46176  ioodvbdlimc2lem  46178  dvnmptdivc  46182  dvxpaek  46184  dvnxpaek  46186  dvnmul  46187  dvnprodlem2  46191  ibliccsinexp  46195  itgsinexplem1  46198  itgsinexp  46199  iblempty  46209  itgcoscmulx  46213  itgsincmulx  46218  itgioocnicc  46221  iblcncfioo  46222  itgsbtaddcnst  46226  volioofmpt  46238  volicofmpt  46241  stoweidlem4  46248  stirlinglem5  46322  dirkerval  46335  dirkertrigeq  46345  dirkeritg  46346  dirkercncflem2  46348  dirkercncflem4  46350  fourierdlem16  46367  fourierdlem18  46369  fourierdlem21  46372  fourierdlem22  46373  fourierdlem28  46379  fourierdlem39  46390  fourierdlem40  46391  fourierdlem41  46392  fourierdlem53  46403  fourierdlem56  46406  fourierdlem57  46407  fourierdlem60  46410  fourierdlem61  46411  fourierdlem68  46418  fourierdlem73  46423  fourierdlem74  46424  fourierdlem75  46425  fourierdlem76  46426  fourierdlem78  46428  fourierdlem81  46431  fourierdlem82  46432  fourierdlem83  46433  fourierdlem84  46434  fourierdlem85  46435  fourierdlem88  46438  fourierdlem90  46440  fourierdlem92  46442  fourierdlem93  46443  fourierdlem95  46445  fourierdlem97  46447  fourierdlem101  46451  fourierdlem103  46453  fourierdlem104  46454  fourierdlem111  46461  fourierdlem112  46462  sqwvfoura  46472  sqwvfourb  46473  fouriersw  46475  elaa2lem  46477  etransclem4  46482  etransclem17  46495  etransclem18  46496  etransclem32  46510  etransclem46  46524  sge0z  46619  sge0revalmpt  46622  sge0tsms  46624  sge0sup  46635  sge0iunmptlemre  46659  sge0iun  46663  sge0xaddlem2  46678  ismeannd  46711  psmeasurelem  46714  meaiuninclem  46724  meaiininclem  46730  caratheodory  46772  isomenndlem  46774  ovnval  46785  hoicvrrex  46800  ovnlecvr  46802  ovncvrrp  46808  ovn0lem  46809  ovnsubaddlem1  46814  hoidmv1lelem2  46836  hoidmv1le  46838  hoidmvlelem3  46841  ovnhoilem2  46846  ovnhoi  46847  ovnlecvr2  46854  ovncvr2  46855  hspmbllem2  46871  ovolval2lem  46887  ovolval3  46891  ovolval5lem1  46896  ovolval5lem2  46897  ovnovollem1  46900  ovnovollem2  46901  vonioolem1  46924  vonicclem1  46927  vonct  46937  smflim  47021  smfinflem  47061  smflimsuplem5  47068  smfliminflem  47074  cfsetsnfsetfv  47303  fundcmpsurbijinjpreimafv  47653  fundcmpsurinjimaid  47657  fdmdifeqresdif  48588  ply1mulgsumlem2  48633  lincvalsc0  48667  linc0scn0  48669  lincdifsn  48670  lincsum  48675  lincscm  48676  lindslinindimp2lem4  48707  lindslinindsimp2lem5  48708  lincresunit3lem2  48726  1arymaptfo  48889  itcovalpclem1  48916  itcovalpclem2  48917  itcovalt2lem1  48921  itcovalt2lem2  48922  tposcurf1  49544  tposcurf2  49545  diag1  49549  fuco22  49584  fucocolem2  49599  fucocolem3  49600  fucocolem4  49601  fucoco  49602  fucolid  49606  fucorid  49607  postcofval  49609  precofval  49612  precofvalALT  49613  precofval2  49614  fucoppcco  49654  islmd  49910  iscmd  49911  aacllem  50046  amgmwlem  50047