Theorem mpteq2dva 5170

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-opab 5133  df-mpt 5154

This theorem is referenced by:  mpteq2dv  5172  mpteq2ia  5173  2fvcoidd  7149  offval  7520  offval2  7531  caofinvl  7541  caofcom  7546  caofass  7548  caofdi  7550  caofdir  7551  caonncan  7552  curry1  7915  curry2  7918  mpocurryd  8056  pw2f1olem  8816  mapxpen  8879  xpmapenlem  8880  cantnfp1  9369  cantnflem1d  9376  cantnflem1  9377  cnfcom2lem  9389  dfac12lem1  9830  seqof  13708  seqof2  13709  swrdswrd  14346  repswswrd  14425  repswrevw  14428  revco  14475  ccatco  14476  repsco  14481  ofccat  14608  lo1eq  15205  rlimeq  15206  lo1mul2  15266  o1dif  15267  lo1sub  15268  rlimdiv  15285  caucvgr  15315  sumeq1  15328  fsumrlim  15451  fsumo1  15452  climfsum  15460  geomulcvg  15516  vdwlem8  16617  prmgapprmo  16691  restid2  17058  pwsplusgval  17118  pwsmulrval  17119  pwsvscafval  17122  qusin  17172  xpsaddlem  17201  xpsvsca  17205  catidd  17306  fuclid  17600  fucrid  17601  fucass  17602  setcepi  17719  prf1st  17837  prf2nd  17838  1st2ndprf  17839  curfcl  17866  curfuncf  17872  diag2  17879  curf2ndf  17881  hof2val  17890  hofcllem  17892  hofcl  17893  yonedalem4a  17909  yonedalem4c  17911  yonedalem3b  17913  yonedainv  17915  yonffthlem  17916  prdsidlem  18332  prdsmndd  18333  pwsco2mhm  18386  frmdup3lem  18420  frmdup3  18421  smndex1gid  18457  smndex1igid  18458  grpinvpropd  18565  prdsinvlem  18599  pwsinvg  18603  pwssub  18604  galactghm  18927  cayleylem1  18935  pmtrprfval  19010  sylow1lem2  19119  sylow3lem1  19147  efginvrel1  19249  frgpup3lem  19298  frgpup3  19299  prdscmnd  19377  iscyggen  19395  gsumval3  19423  gsumcllem  19424  gsumzsplit  19443  gsumsub  19464  gsummptf1o  19479  gsum2d  19488  gsum2d2  19490  gsumxp  19492  prdsgsum  19497  telgsumfz  19506  telgsumfz0  19508  telgsum  19510  dprdfsub  19539  dprdfeq0  19540  dprddisj2  19557  dprd2d2  19562  dpjidcl  19576  ablfaclem2  19604  ablfac2  19607  srgbinomlem3  19693  srgbinomlem4  19694  srgbinomlem  19695  gsumdixp  19763  prdsmgp  19764  prdsringd  19766  prdslmodd  20146  mulgrhm2  20612  frgpcyg  20693  evpmodpmf1o  20713  phlpropd  20772  frlmphl  20898  uvcresum  20910  frlmup1  20915  asclpropd  21011  psrass1lemOLD  21053  psrass1lem  21056  psrlinv  21076  psrass1  21084  psrdi  21085  psrdir  21086  psrass23l  21087  psrcom  21088  psrass23  21089  resspsrmul  21096  mplsubrglem  21120  mplmonmul  21147  mplcoe1  21148  mplcoe5  21151  mplcoe4  21189  evlslem3  21200  evlslem1  21202  mhpmulcl  21249  psrplusgpropd  21317  psropprmul  21319  coe1mul2  21350  coe1tm  21354  coe1tmmul2  21357  coe1tmmul  21358  coe1pwmul  21360  cply1mul  21375  ply1coe  21377  eqcoe1ply1eq  21378  lply1binomsc  21388  evl1gsummon  21441  mamures  21449  grpvrinv  21455  mhmvlin  21456  mamuass  21459  mamudi  21460  mamudir  21461  mamuvs1  21462  mamuvs2  21463  mpomatmul  21503  mamutpos  21515  madetsumid  21518  dmatmul  21554  scmatscm  21570  1mavmul  21605  mavmulass  21606  mvmumamul1  21611  mulmarep1gsum1  21630  mulmarep1gsum2  21631  mdetleib2  21645  mdetfval1  21647  mdet0pr  21649  mdetdiag  21656  mdetdiagid  21657  mdetrlin  21659  mdetrsca  21660  mdetralt  21665  mdetunilem9  21677  gsummatr01  21716  smadiadetlem1a  21720  smadiadetlem3  21725  smadiadetlem4  21726  cpmatmcllem  21775  mat2pmatmul  21788  decpmatmullem  21828  decpmatmul  21829  pmatcollpw1lem2  21832  pmatcollpw  21838  pmatcollpw3lem  21840  pmatcollpwscmat  21848  idpm2idmp  21858  mp2pm2mplem3  21865  mp2pm2mplem4  21866  mp2pm2mplem5  21867  mp2pm2mp  21868  pm2mpghm  21873  pm2mpmhmlem2  21876  monmat2matmon  21881  pm2mp  21882  chpdmat  21898  chpscmat  21899  chpscmatgsumbin  21901  chpscmatgsummon  21902  chp0mat  21903  chpidmat  21904  chfacfscmulgsum  21917  chfacfpmmulgsum  21921  chfacfpmmulgsum2  21922  cayhamlem1  21923  cpmidgsumm2pm  21926  cpmidpmat  21930  cpmadugsumlemB  21931  cpmadugsumlemC  21932  cpmadugsumlemF  21933  cpmadumatpoly  21940  cayhamlem3  21944  cayhamlem4  21945  cayleyhamilton0  21946  cayleyhamiltonALT  21948  neiptopnei  22191  neiptopreu  22192  ptcnplem  22680  cnmpt1t  22724  cnmpt12  22726  cnmptkp  22739  cnmptk1  22740  cnmpt1k  22741  cnmptkk  22742  cnmptk1p  22744  cnmpt2k  22747  qtopeu  22775  pt1hmeo  22865  ptunhmeo  22867  xkocnv  22873  xkohmeo  22874  flfcnp2  23066  cnmpt1plusg  23146  istgp2  23150  tmdmulg  23151  tgpmulg  23152  tmdgsum  23154  subgtgp  23164  symgtgp  23165  tgpconncomp  23172  prdstgpd  23184  tsmsmhm  23205  tsmsadd  23206  tsmssub  23208  tgptsmscls  23209  tsmssplit  23211  tsmsxplem1  23212  tsmsxplem2  23213  cnmpt1vsca  23253  tlmtgp  23255  ustuqtoplem  23299  utopsnneip  23308  ressprdsds  23432  metuval  23611  nmfval0  23652  tngnm  23721  nmoeq0  23806  idnghm  23813  cnmpt1ds  23911  fsumcn  23939  expcn  23941  divccn  23942  divccncf  23975  negcncf  23991  copco  24087  pcopt  24091  pcopt2  24092  pcoass  24093  pi1xfrcnvlem  24125  cnmpt1ip  24316  rrxnm  24460  rrxds  24462  minveclem3b  24497  divcncf  24516  ovolctb  24559  ovoliunnul  24576  voliunlem3  24621  ovolfs2  24640  uniioombllem2  24652  vitalilem4  24680  vitalilem5  24681  ismbf  24697  mbfss  24715  mbfmulc2re  24717  mbfneg  24719  mbfpos  24720  mbfposb  24722  mbfadd  24730  mbfsub  24731  mbfmulc2  24732  mbfinf  24734  mbflimsup  24735  mbflimlem  24736  i1fpos  24776  i1fposd  24777  itg1climres  24784  mbfmul  24796  itg2mulc  24817  itg2i1fseq  24825  itg2cnlem1  24831  itg2cnlem2  24832  itgresr  24848  iblneg  24872  i1fibl  24877  itgitg1  24878  iblsub  24891  itgfsum  24896  itgmulc2lem1  24901  limcmpt  24952  limccnp  24960  limcco  24962  dvreslem  24978  dvres2lem  24979  dvidlem  24984  dvcnp2  24989  dvaddbr  25007  dvmulbr  25008  dvmulf  25012  dvcmulf  25014  dvcobr  25015  dvcof  25017  dvcjbr  25018  dvcj  25019  dvfre  25020  dvexp  25022  dvexp2  25023  dvrec  25024  dvmptcmul  25033  dvmptdivc  25034  dvmptneg  25035  dvmptsub  25036  dvmptre  25038  dvmptim  25039  dvrecg  25042  dvmptdiv  25043  dvmptfsum  25044  dvcnvlem  25045  dvcnv  25046  dvexp3  25047  dvef  25049  dvsincos  25050  dv11cn  25070  lhop2  25084  lhop  25085  ftc2  25113  itgparts  25116  itgsubstlem  25117  mdegfval  25132  mdegmullem  25148  ply1termlem  25269  plypow  25271  plyconst  25272  plyeq0lem  25276  plypf1  25278  plyaddlem1  25279  plymullem1  25280  coeeulem  25290  coeidlem  25303  plyco  25307  coeeq2  25308  0dgr  25311  0dgrb  25312  dgrcolem1  25339  dgrcolem2  25340  plycjlem  25342  dvply1  25349  dvply2g  25350  plydiveu  25363  plyremlem  25369  elqaalem3  25386  taylfval  25423  dvtaylp  25434  taylthlem1  25437  taylthlem2  25438  ulmshft  25454  mtestbdd  25469  iblulm  25471  itgulm2  25473  pserulm  25486  psercn2  25487  pserdvlem2  25492  pserdv  25493  pserdv2  25494  abelthlem1  25495  abelthlem3  25497  advlog  25714  advlogexp  25715  dvcxp1  25798  dvcxp2  25799  dvcncxp1  25801  sqrtcn  25808  loglesqrt  25816  dvatan  25990  atantayl2  25993  atantayl3  25994  leibpi  25997  rlimcnp2  26021  efrlim  26024  dfef2  26025  cxp2lim  26031  divsqrtsumlem  26034  lgamgulmlem2  26084  lgamgulm2  26090  lgamcvglem  26094  gamcvg2lem  26113  ftalem7  26133  basellem9  26143  muinv  26247  logfacrlim  26277  logexprlim  26278  dchrmulid2  26305  dchrinvcl  26306  lgseisenlem3  26430  lgseisenlem4  26431  chtppilimlem2  26527  chebbnd2  26530  chpchtlim  26532  chpo1ub  26533  rpvmasumlem  26540  dchrmusumlema  26546  dchrvmasumlem1  26548  dchrvmasumiflem2  26555  dchrisum0fno1  26564  rpvmasum2  26565  dchrisum0lema  26567  dchrisum0lem1  26569  dchrisum0lem2a  26570  dchrisum0lem2  26571  dchrisum0  26573  dchrmusumlem  26575  dchrvmasumlem  26576  rpvmasum  26579  rplogsum  26580  logdivsum  26586  mulog2sumlem3  26589  vmalogdivsum2  26591  vmalogdivsum  26592  2vmadivsumlem  26593  logsqvma2  26596  log2sumbnd  26597  selberglem2  26599  selberg3lem1  26610  selberg3  26612  selberg4lem1  26613  selberg4  26614  pntrsumo1  26618  selberg3r  26622  selberg4r  26623  selberg34r  26624  pntrlog2bndlem2  26631  pntrlog2bndlem4  26633  pntrlog2bndlem5  26634  pntrlog2bndlem6  26636  padicabvf  26684  padicabvcxp  26685  mirval  26920  crctcshlem4  28086  clwlknf1oclwwlkn  28349  eucrct2eupth  28510  chscllem4  29903  brafnmul  30214  kbmul  30218  cofmpt2  30870  ofresid  30880  ofoprabco  30903  fcobijfs  30960  gsummpt2d  31211  gsummptres  31214  gsummptres2  31215  gsumpart  31217  gsumhashmul  31218  fzto1st1  31271  fzto1st  31272  freshmansdream  31386  qusima  31496  elrspunidl  31508  lbsdiflsp0  31609  fedgmullem1  31612  fedgmullem2  31613  mdetpmtr1  31675  mdetlap  31684  xrge0mulc1cn  31793  esumval  31914  esumsnf  31932  esumpcvgval  31946  esumcvg  31954  esumcvgsum  31956  esumsup  31957  ofcfeqd2  31969  meascnbl  32087  sitgval  32199  probmeasb  32297  cndprobprob  32305  dstfrvclim1  32344  ballotlemfval  32356  ballotlemsval  32375  ballotlemieq  32383  plymul02  32425  plymulx0  32426  plymulx  32427  signsplypnf  32429  signstfv  32442  signstfvn  32448  signstfvp  32450  itgexpif  32486  logdivsqrle  32530  ptpconn  33095  cvmliftlem6  33152  cvmliftphtlem  33179  cvmlift3lem5  33185  elmrsubrn  33382  msubfval  33386  msubco  33393  divcnvlin  33604  knoppcnlem9  34608  knoppcnlem10  34609  knoppcnlem11  34610  bj-finsumval0  35383  curf  35682  matunitlindflem1  35700  matunitlindflem2  35701  poimirlem3  35707  poimirlem15  35719  poimirlem16  35720  poimirlem17  35721  poimirlem19  35723  poimirlem20  35724  broucube  35738  ovoliunnfl  35746  voliunnfl  35748  volsupnfl  35749  mbfposadd  35751  itg2addnclem  35755  itg2addnclem3  35757  itg2addnc  35758  itgaddnclem2  35763  itgaddnc  35764  iblsubnc  35765  itgsubnc  35766  itgmulc2nclem1  35770  itgmulc2nclem2  35771  itgmulc2nc  35772  itgabsnc  35773  ftc1cnnclem  35775  ftc1anclem3  35779  ftc1anclem5  35781  ftc1anclem6  35782  ftc1anclem8  35784  ftc1anc  35785  ftc2nc  35786  areacirclem1  35792  areacirclem2  35793  areacirclem4  35795  areacirc  35797  upixp  35814  lcmineqlem8  39972  lcmineqlem12  39976  dvrelog2b  40002  dvrelogpow2b  40004  aks4d1p1p6  40009  aks4d1p1p5  40011  sticksstones12a  40041  sticksstones12  40042  sticksstones19  40049  qsalrel  40141  pwsgprod  40194  evlsbagval  40198  fsuppssindlem1  40203  fsuppssind  40205  mhphf  40208  mzpsubst  40486  mzprename  40487  mzpcompact2lem  40489  eldioph2  40500  rabdiophlem2  40540  mendlmod  40934  mendassa  40935  areaquad  40963  fsovcnvlem  41510  hashnzfzclim  41829  expgrowthi  41840  expgrowth  41842  uzmptshftfval  41853  dvradcnv2  41854  binomcxplemrat  41857  binomcxplemfrat  41858  binomcxplemradcnv  41859  binomcxplemdvbinom  41860  binomcxplemcvg  41861  binomcxplemdvsum  41862  binomcxplemnotnn0  41863  mulc1cncfg  43020  expcnfg  43022  fprodcnlem  43030  clim1fr1  43032  divcnvg  43058  sublimc  43083  reclimc  43084  divlimc  43087  limsupresico  43131  limsuppnfdlem  43132  limsupvaluz  43139  supcnvlimsupmpt  43172  liminfresico  43202  climliminflimsupd  43232  cncfmptssg  43302  negcncfg  43312  cncficcgt0  43319  fprodcncf  43331  fprodsubrecnncnvlem  43338  fprodaddrecnncnvlem  43340  dvsinax  43344  dvasinbx  43351  dvdivf  43353  ioodvbdlimc1lem2  43363  ioodvbdlimc2lem  43365  dvnmptdivc  43369  dvxpaek  43371  dvnxpaek  43373  dvnmul  43374  dvnprodlem2  43378  ibliccsinexp  43382  itgsinexplem1  43385  itgsinexp  43386  iblempty  43396  itgcoscmulx  43400  itgsincmulx  43405  itgioocnicc  43408  iblcncfioo  43409  itgsbtaddcnst  43413  volioofmpt  43425  volicofmpt  43428  stoweidlem4  43435  stirlinglem5  43509  dirkerval  43522  dirkertrigeq  43532  dirkeritg  43533  dirkercncflem2  43535  dirkercncflem4  43537  fourierdlem16  43554  fourierdlem18  43556  fourierdlem21  43559  fourierdlem22  43560  fourierdlem28  43566  fourierdlem39  43577  fourierdlem40  43578  fourierdlem41  43579  fourierdlem53  43590  fourierdlem56  43593  fourierdlem57  43594  fourierdlem60  43597  fourierdlem61  43598  fourierdlem68  43605  fourierdlem73  43610  fourierdlem74  43611  fourierdlem75  43612  fourierdlem76  43613  fourierdlem78  43615  fourierdlem81  43618  fourierdlem82  43619  fourierdlem83  43620  fourierdlem84  43621  fourierdlem85  43622  fourierdlem88  43625  fourierdlem90  43627  fourierdlem92  43629  fourierdlem93  43630  fourierdlem95  43632  fourierdlem97  43634  fourierdlem101  43638  fourierdlem103  43640  fourierdlem104  43641  fourierdlem111  43648  fourierdlem112  43649  sqwvfoura  43659  sqwvfourb  43660  fouriersw  43662  elaa2lem  43664  etransclem4  43669  etransclem17  43682  etransclem18  43683  etransclem32  43697  etransclem46  43711  sge0z  43803  sge0revalmpt  43806  sge0tsms  43808  sge0sup  43819  sge0iunmptlemre  43843  sge0iun  43847  sge0xaddlem2  43862  ismeannd  43895  psmeasurelem  43898  meaiuninclem  43908  meaiininclem  43914  caratheodory  43956  isomenndlem  43958  ovnval  43969  hoicvrrex  43984  ovnlecvr  43986  ovncvrrp  43992  ovn0lem  43993  ovnsubaddlem1  43998  hoidmv1lelem2  44020  hoidmv1le  44022  hoidmvlelem3  44025  ovnhoilem2  44030  ovnhoi  44031  ovnlecvr2  44038  ovncvr2  44039  hspmbllem2  44055  ovolval2lem  44071  ovolval3  44075  ovolval5lem1  44080  ovolval5lem2  44081  ovnovollem1  44084  ovnovollem2  44085  vonioolem1  44108  vonicclem1  44111  vonct  44121  smflim  44199  smfinflem  44237  smflimsuplem5  44244  smfliminflem  44250  cfsetsnfsetfv  44438  fundcmpsurbijinjpreimafv  44747  fundcmpsurinjimaid  44751  fdmdifeqresdif  45565  ply1mulgsumlem2  45616  lincvalsc0  45650  linc0scn0  45652  lincdifsn  45653  lincsum  45658  lincscm  45659  lindslinindimp2lem4  45690  lindslinindsimp2lem5  45691  lincresunit3lem2  45709  1arymaptfo  45877  itcovalpclem1  45904  itcovalpclem2  45905  itcovalt2lem1  45909  itcovalt2lem2  45910  aacllem  46391  amgmwlem  46392