Theorem mpteq2dva 5200

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 5193	1 ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵) = (𝑥 ∈ 𝐴 ↦ 𝐶))

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1540   ∈ wcel 2109   ↦ cmpt 5188

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 5170  df-mpt 5189

This theorem is referenced by:  mpteq2dv  5201  mpteq2ia  5202  2fvcoidd  7272  offval  7662  offval2  7673  coof  7677  caofinvl  7685  caofcom  7690  caofass  7693  caofdi  7695  caofdir  7696  caonncan  7697  curry1  8083  curry2  8086  mpocurryd  8248  pw2f1olem  9045  mapxpen  9107  xpmapenlem  9108  cantnfp1  9634  cantnflem1d  9641  cantnflem1  9642  cnfcom2lem  9654  dfac12lem1  10097  seqof  14024  seqof2  14025  swrdswrd  14670  repswswrd  14749  repswrevw  14752  revco  14800  ccatco  14801  repsco  14806  ofccat  14935  lo1eq  15534  rlimeq  15535  lo1mul2  15595  o1dif  15596  lo1sub  15597  rlimdiv  15612  caucvgr  15642  sumeq1  15655  fsumrlim  15777  fsumo1  15778  climfsum  15786  geomulcvg  15842  vdwlem8  16959  prmgapprmo  17033  restid2  17393  pwsplusgval  17453  pwsmulrval  17454  pwsvscafval  17457  qusin  17507  xpsaddlem  17536  xpsvsca  17540  catidd  17641  fuclid  17931  fucrid  17932  fucass  17933  setcepi  18050  prf1st  18165  prf2nd  18166  1st2ndprf  18167  curfcl  18193  curfuncf  18199  diag2  18206  curf2ndf  18208  hof2val  18217  hofcllem  18219  hofcl  18220  yonedalem4a  18236  yonedalem4c  18238  yonedalem3b  18240  yonedainv  18242  yonffthlem  18243  prdssgrpd  18660  prdsidlem  18696  prdsmndd  18697  mhmvlin  18728  pwsco2mhm  18760  frmdup3lem  18793  frmdup3  18794  smndex1gid  18830  smndex1igid  18831  grpinvpropd  18947  prdsinvlem  18981  pwsinvg  18985  pwssub  18986  galactghm  19334  cayleylem1  19342  pmtrprfval  19417  sylow1lem2  19529  sylow3lem1  19557  efginvrel1  19658  frgpup3lem  19707  frgpup3  19708  prdscmnd  19791  iscyggen  19810  gsumval3  19837  gsumcllem  19838  gsumzsplit  19857  gsumsub  19878  gsummptf1o  19893  gsum2d  19902  gsum2d2  19904  gsumxp  19906  prdsgsum  19911  telgsumfz  19920  telgsumfz0  19922  telgsum  19924  dprdfsub  19953  dprdfeq0  19954  dprddisj2  19971  dprd2d2  19976  dpjidcl  19990  ablfaclem2  20018  ablfac2  20021  prdsmgp  20060  prdsrngd  20085  srgbinomlem3  20137  srgbinomlem4  20138  srgbinomlem  20139  gsumdixp  20228  prdsringd  20230  prdslmodd  20875  mulgrhm2  21388  frgpcyg  21483  freshmansdream  21484  evpmodpmf1o  21505  phlpropd  21564  frlmphl  21690  uvcresum  21702  frlmup1  21707  asclpropd  21806  psrass1lem  21841  psrlinv  21864  psrass1  21873  psrdi  21874  psrdir  21875  psrass23l  21876  psrcom  21877  psrass23  21878  resspsrmul  21885  mplsubrglem  21913  mplmonmul  21943  mplcoe1  21944  mplcoe5  21947  mplcoe4  21978  evlslem3  21987  evlslem1  21989  mhpmulcl  22036  psdmplcl  22049  psdadd  22050  psdmul  22053  psdmvr  22056  psrplusgpropd  22120  psropprmul  22122  coe1mul2  22155  coe1tm  22159  coe1tmmul2  22162  coe1tmmul  22163  coe1pwmul  22165  cply1mul  22183  ply1coe  22185  eqcoe1ply1eq  22186  lply1binomsc  22198  evl1gsummon  22252  evls1fpws  22256  rhmcomulmpl  22269  mamures  22284  grpvrinv  22286  mamuass  22289  mamudi  22290  mamudir  22291  mamuvs1  22292  mamuvs2  22293  mpomatmul  22333  mamutpos  22345  madetsumid  22348  dmatmul  22384  scmatscm  22400  1mavmul  22435  mavmulass  22436  mvmumamul1  22441  mulmarep1gsum1  22460  mulmarep1gsum2  22461  mdetleib2  22475  mdetfval1  22477  mdet0pr  22479  mdetdiag  22486  mdetdiagid  22487  mdetrlin  22489  mdetrsca  22490  mdetralt  22495  mdetunilem9  22507  gsummatr01  22546  smadiadetlem1a  22550  smadiadetlem3  22555  smadiadetlem4  22556  cpmatmcllem  22605  mat2pmatmul  22618  decpmatmullem  22658  decpmatmul  22659  pmatcollpw1lem2  22662  pmatcollpw  22668  pmatcollpw3lem  22670  pmatcollpwscmat  22678  idpm2idmp  22688  mp2pm2mplem3  22695  mp2pm2mplem4  22696  mp2pm2mplem5  22697  mp2pm2mp  22698  pm2mpghm  22703  pm2mpmhmlem2  22706  monmat2matmon  22711  pm2mp  22712  chpdmat  22728  chpscmat  22729  chpscmatgsumbin  22731  chpscmatgsummon  22732  chp0mat  22733  chpidmat  22734  chfacfscmulgsum  22747  chfacfpmmulgsum  22751  chfacfpmmulgsum2  22752  cayhamlem1  22753  cpmidgsumm2pm  22756  cpmidpmat  22760  cpmadugsumlemB  22761  cpmadugsumlemC  22762  cpmadugsumlemF  22763  cpmadumatpoly  22770  cayhamlem3  22774  cayhamlem4  22775  cayleyhamilton0  22776  cayleyhamiltonALT  22778  neiptopnei  23019  neiptopreu  23020  ptcnplem  23508  cnmpt1t  23552  cnmpt12  23554  cnmptkp  23567  cnmptk1  23568  cnmpt1k  23569  cnmptkk  23570  cnmptk1p  23572  cnmpt2k  23575  qtopeu  23603  pt1hmeo  23693  ptunhmeo  23695  xkocnv  23701  xkohmeo  23702  flfcnp2  23894  cnmpt1plusg  23974  istgp2  23978  tmdmulg  23979  tgpmulg  23980  tmdgsum  23982  subgtgp  23992  symgtgp  23993  tgpconncomp  24000  prdstgpd  24012  tsmsmhm  24033  tsmsadd  24034  tsmssub  24036  tgptsmscls  24037  tsmssplit  24039  tsmsxplem1  24040  tsmsxplem2  24041  cnmpt1vsca  24081  tlmtgp  24083  ustuqtoplem  24127  utopsnneip  24136  ressprdsds  24259  metuval  24437  nmfval0  24478  tngnm  24539  nmoeq0  24624  idnghm  24631  cnmpt1ds  24731  fsumcn  24761  expcn  24763  divccn  24764  expcnOLD  24765  divccnOLD  24766  divccncf  24799  negcncf  24815  negcncfOLD  24816  copco  24918  pcopt  24922  pcopt2  24923  pcoass  24924  pi1xfrcnvlem  24956  cnmpt1ip  25147  rrxnm  25291  rrxds  25293  minveclem3b  25328  divcncf  25348  ovolctb  25391  ovoliunnul  25408  voliunlem3  25453  ovolfs2  25472  uniioombllem2  25484  vitalilem4  25512  vitalilem5  25513  ismbf  25529  mbfss  25547  mbfmulc2re  25549  mbfneg  25551  mbfpos  25552  mbfposb  25554  mbfadd  25562  mbfsub  25563  mbfmulc2  25564  mbfinf  25566  mbflimsup  25567  mbflimlem  25568  i1fpos  25607  i1fposd  25608  itg1climres  25615  mbfmul  25627  itg2mulc  25648  itg2i1fseq  25656  itg2cnlem1  25662  itg2cnlem2  25663  itgresr  25680  iblneg  25704  i1fibl  25709  itgitg1  25710  iblsub  25723  itgfsum  25728  itgmulc2lem1  25733  limcmpt  25784  limccnp  25792  limcco  25794  dvreslem  25810  dvres2lem  25811  dvidlem  25816  dvcnp2  25821  dvcnp2OLD  25822  dvaddbr  25840  dvmulbr  25841  dvmulbrOLD  25842  dvmulf  25846  dvcmulf  25848  dvcobr  25849  dvcobrOLD  25850  dvcof  25852  dvcjbr  25853  dvcj  25854  dvfre  25855  dvexp  25857  dvexp2  25858  dvrec  25859  dvmptcmul  25868  dvmptdivc  25869  dvmptneg  25870  dvmptsub  25871  dvmptre  25873  dvmptim  25874  dvrecg  25877  dvmptdiv  25878  dvmptfsum  25879  dvcnvlem  25880  dvcnv  25881  dvexp3  25882  dvef  25884  dvsincos  25885  dv11cn  25906  lhop2  25920  lhop  25921  ftc2  25951  itgparts  25954  itgsubstlem  25955  mdegfval  25967  mdegmullem  25983  ply1termlem  26108  plypow  26110  plyconst  26111  plyeq0lem  26115  plypf1  26117  plyaddlem1  26118  plymullem1  26119  coeeulem  26129  coeidlem  26142  plyco  26146  coeeq2  26147  0dgr  26150  0dgrb  26151  dgrcolem1  26179  dgrcolem2  26180  plycjlem  26182  dvply1  26191  dvply2g  26192  dvply2gOLD  26193  plydiveu  26206  plyremlem  26212  elqaalem3  26229  taylfval  26266  dvtaylp  26278  taylthlem1  26281  taylthlem2  26282  taylthlem2OLD  26283  ulmshft  26299  mtestbdd  26314  iblulm  26316  itgulm2  26318  pserulm  26331  psercn2  26332  psercn2OLD  26333  pserdvlem2  26338  pserdv  26339  pserdv2  26340  abelthlem1  26341  abelthlem3  26343  advlog  26563  advlogexp  26564  dvcxp1  26649  dvcxp2  26650  dvcncxp1  26652  sqrtcn  26660  loglesqrt  26671  dvatan  26845  atantayl2  26848  atantayl3  26849  leibpi  26852  rlimcnp2  26876  efrlim  26879  efrlimOLD  26880  dfef2  26881  cxp2lim  26887  divsqrtsumlem  26890  lgamgulmlem2  26940  lgamgulm2  26946  lgamcvglem  26950  gamcvg2lem  26969  ftalem7  26989  basellem9  26999  muinv  27103  logfacrlim  27135  logexprlim  27136  dchrmullid  27163  dchrinvcl  27164  lgseisenlem3  27288  lgseisenlem4  27289  chtppilimlem2  27385  chebbnd2  27388  chpchtlim  27390  chpo1ub  27391  rpvmasumlem  27398  dchrmusumlema  27404  dchrvmasumlem1  27406  dchrvmasumiflem2  27413  dchrisum0fno1  27422  rpvmasum2  27423  dchrisum0lema  27425  dchrisum0lem1  27427  dchrisum0lem2a  27428  dchrisum0lem2  27429  dchrisum0  27431  dchrmusumlem  27433  dchrvmasumlem  27434  rpvmasum  27437  rplogsum  27438  logdivsum  27444  mulog2sumlem3  27447  vmalogdivsum2  27449  vmalogdivsum  27450  2vmadivsumlem  27451  logsqvma2  27454  log2sumbnd  27455  selberglem2  27457  selberg3lem1  27468  selberg3  27470  selberg4lem1  27471  selberg4  27472  pntrsumo1  27476  selberg3r  27480  selberg4r  27481  selberg34r  27482  pntrlog2bndlem2  27489  pntrlog2bndlem4  27491  pntrlog2bndlem5  27492  pntrlog2bndlem6  27494  padicabvf  27542  padicabvcxp  27543  mirval  28582  crctcshlem4  29750  clwlknf1oclwwlkn  30013  eucrct2eupth  30174  chscllem4  31569  brafnmul  31880  kbmul  31884  cofmpt2  32558  ofresid  32566  ofoprabco  32588  fmptunsnop  32623  fcobijfs  32646  gsummpt2d  32989  gsummptres  32992  gsummptres2  32993  gsummptfsf1o  32994  gsumfs2d  32995  gsumpart  32997  gsumhashmul  33001  gsumwrd2dccat  33007  fzto1st1  33059  fzto1st  33060  elrgspnlem1  33193  elrgspnlem2  33194  elrgspnlem3  33195  elrgspnlem4  33196  elrgspnsubrunlem1  33198  elrgspnsubrunlem2  33199  qusbas2  33377  qusima  33379  elrspunidl  33399  elrspunsn  33400  rprmdvdsprod  33505  ressply1evls1  33534  evl1deg1  33545  evl1deg2  33546  evl1deg3  33547  gsummoncoe1fzo  33563  lbsdiflsp0  33622  fedgmullem1  33625  fedgmullem2  33626  fldextrspunlsplem  33668  fldextrspunlsp  33669  mdetpmtr1  33813  mdetlap  33822  xrge0mulc1cn  33931  esumval  34036  esumsnf  34054  esumpcvgval  34068  esumcvg  34076  esumcvgsum  34078  esumsup  34079  ofcfeqd2  34091  meascnbl  34209  sitgval  34323  probmeasb  34421  cndprobprob  34429  dstfrvclim1  34469  ballotlemfval  34481  ballotlemsval  34500  ballotlemieq  34508  plymul02  34537  plymulx0  34538  plymulx  34539  signsplypnf  34541  signstfv  34554  signstfvn  34560  signstfvp  34562  itgexpif  34597  logdivsqrle  34641  ptpconn  35220  cvmliftlem6  35277  cvmliftphtlem  35304  cvmlift3lem5  35310  elmrsubrn  35507  msubfval  35511  msubco  35518  divcnvlin  35720  knoppcnlem9  36489  knoppcnlem10  36490  knoppcnlem11  36491  bj-finsumval0  37273  curf  37592  matunitlindflem1  37610  matunitlindflem2  37611  poimirlem3  37617  poimirlem15  37629  poimirlem16  37630  poimirlem17  37631  poimirlem19  37633  poimirlem20  37634  broucube  37648  ovoliunnfl  37656  voliunnfl  37658  volsupnfl  37659  mbfposadd  37661  itg2addnclem  37665  itg2addnclem3  37667  itg2addnc  37668  itgaddnclem2  37673  itgaddnc  37674  iblsubnc  37675  itgsubnc  37676  itgmulc2nclem1  37680  itgmulc2nclem2  37681  itgmulc2nc  37682  itgabsnc  37683  ftc1cnnclem  37685  ftc1anclem3  37689  ftc1anclem5  37691  ftc1anclem6  37692  ftc1anclem8  37694  ftc1anc  37695  ftc2nc  37696  areacirclem1  37702  areacirclem2  37703  areacirclem4  37705  areacirc  37707  upixp  37723  lcmineqlem8  42024  lcmineqlem12  42028  dvrelog2b  42054  dvrelogpow2b  42056  aks4d1p1p6  42061  aks4d1p1p5  42063  aks6d1c1  42104  aks6d1c5lem3  42125  sticksstones12a  42145  sticksstones12  42146  sticksstones19  42153  aks6d1c6lem1  42158  aks6d1c6lem4  42161  aks6d1c7lem3  42170  qsalrel  42228  pwsgprod  42532  rhmcomulpsr  42539  evlsvvval  42551  evlsevl  42559  selvvvval  42573  evlselv  42575  fsuppssindlem1  42579  fsuppssind  42581  mhphf  42585  mzpsubst  42736  mzprename  42737  mzpcompact2lem  42739  eldioph2  42750  rabdiophlem2  42790  mendlmod  43178  mendassa  43179  areaquad  43205  fsovcnvlem  44002  hashnzfzclim  44311  expgrowthi  44322  expgrowth  44324  uzmptshftfval  44335  dvradcnv2  44336  binomcxplemrat  44339  binomcxplemfrat  44340  binomcxplemradcnv  44341  binomcxplemdvbinom  44342  binomcxplemcvg  44343  binomcxplemdvsum  44344  binomcxplemnotnn0  44345  mulc1cncfg  45587  expcnfg  45589  fprodcnlem  45597  clim1fr1  45599  divcnvg  45625  sublimc  45650  reclimc  45651  divlimc  45654  limsupresico  45698  limsuppnfdlem  45699  limsupvaluz  45706  supcnvlimsupmpt  45739  liminfresico  45769  climliminflimsupd  45799  cncfmptssg  45869  negcncfg  45879  cncficcgt0  45886  fprodcncf  45898  fprodsubrecnncnvlem  45905  fprodaddrecnncnvlem  45907  dvsinax  45911  dvasinbx  45918  dvdivf  45920  ioodvbdlimc1lem2  45930  ioodvbdlimc2lem  45932  dvnmptdivc  45936  dvxpaek  45938  dvnxpaek  45940  dvnmul  45941  dvnprodlem2  45945  ibliccsinexp  45949  itgsinexplem1  45952  itgsinexp  45953  iblempty  45963  itgcoscmulx  45967  itgsincmulx  45972  itgioocnicc  45975  iblcncfioo  45976  itgsbtaddcnst  45980  volioofmpt  45992  volicofmpt  45995  stoweidlem4  46002  stirlinglem5  46076  dirkerval  46089  dirkertrigeq  46099  dirkeritg  46100  dirkercncflem2  46102  dirkercncflem4  46104  fourierdlem16  46121  fourierdlem18  46123  fourierdlem21  46126  fourierdlem22  46127  fourierdlem28  46133  fourierdlem39  46144  fourierdlem40  46145  fourierdlem41  46146  fourierdlem53  46157  fourierdlem56  46160  fourierdlem57  46161  fourierdlem60  46164  fourierdlem61  46165  fourierdlem68  46172  fourierdlem73  46177  fourierdlem74  46178  fourierdlem75  46179  fourierdlem76  46180  fourierdlem78  46182  fourierdlem81  46185  fourierdlem82  46186  fourierdlem83  46187  fourierdlem84  46188  fourierdlem85  46189  fourierdlem88  46192  fourierdlem90  46194  fourierdlem92  46196  fourierdlem93  46197  fourierdlem95  46199  fourierdlem97  46201  fourierdlem101  46205  fourierdlem103  46207  fourierdlem104  46208  fourierdlem111  46215  fourierdlem112  46216  sqwvfoura  46226  sqwvfourb  46227  fouriersw  46229  elaa2lem  46231  etransclem4  46236  etransclem17  46249  etransclem18  46250  etransclem32  46264  etransclem46  46278  sge0z  46373  sge0revalmpt  46376  sge0tsms  46378  sge0sup  46389  sge0iunmptlemre  46413  sge0iun  46417  sge0xaddlem2  46432  ismeannd  46465  psmeasurelem  46468  meaiuninclem  46478  meaiininclem  46484  caratheodory  46526  isomenndlem  46528  ovnval  46539  hoicvrrex  46554  ovnlecvr  46556  ovncvrrp  46562  ovn0lem  46563  ovnsubaddlem1  46568  hoidmv1lelem2  46590  hoidmv1le  46592  hoidmvlelem3  46595  ovnhoilem2  46600  ovnhoi  46601  ovnlecvr2  46608  ovncvr2  46609  hspmbllem2  46625  ovolval2lem  46641  ovolval3  46645  ovolval5lem1  46650  ovolval5lem2  46651  ovnovollem1  46654  ovnovollem2  46655  vonioolem1  46678  vonicclem1  46681  vonct  46691  smflim  46775  smfinflem  46815  smflimsuplem5  46822  smfliminflem  46828  cfsetsnfsetfv  47058  fundcmpsurbijinjpreimafv  47408  fundcmpsurinjimaid  47412  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