Theorem mpteq2dva 5242

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

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

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 2007  ax-8 2110  ax-9 2118  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-opab 5206  df-mpt 5226

This theorem is referenced by:  mpteq2dv  5244  mpteq2ia  5245  2fvcoidd  7317  offval  7706  offval2  7717  coof  7721  caofinvl  7729  caofcom  7734  caofass  7737  caofdi  7739  caofdir  7740  caonncan  7741  curry1  8129  curry2  8132  mpocurryd  8294  pw2f1olem  9116  mapxpen  9183  xpmapenlem  9184  cantnfp1  9721  cantnflem1d  9728  cantnflem1  9729  cnfcom2lem  9741  dfac12lem1  10184  seqof  14100  seqof2  14101  swrdswrd  14743  repswswrd  14822  repswrevw  14825  revco  14873  ccatco  14874  repsco  14879  ofccat  15008  lo1eq  15604  rlimeq  15605  lo1mul2  15665  o1dif  15666  lo1sub  15667  rlimdiv  15682  caucvgr  15712  sumeq1  15725  fsumrlim  15847  fsumo1  15848  climfsum  15856  geomulcvg  15912  vdwlem8  17026  prmgapprmo  17100  restid2  17475  pwsplusgval  17535  pwsmulrval  17536  pwsvscafval  17539  qusin  17589  xpsaddlem  17618  xpsvsca  17622  catidd  17723  fuclid  18014  fucrid  18015  fucass  18016  setcepi  18133  prf1st  18249  prf2nd  18250  1st2ndprf  18251  curfcl  18277  curfuncf  18283  diag2  18290  curf2ndf  18292  hof2val  18301  hofcllem  18303  hofcl  18304  yonedalem4a  18320  yonedalem4c  18322  yonedalem3b  18324  yonedainv  18326  yonffthlem  18327  prdssgrpd  18746  prdsidlem  18782  prdsmndd  18783  mhmvlin  18814  pwsco2mhm  18846  frmdup3lem  18879  frmdup3  18880  smndex1gid  18916  smndex1igid  18917  grpinvpropd  19033  prdsinvlem  19067  pwsinvg  19071  pwssub  19072  galactghm  19422  cayleylem1  19430  pmtrprfval  19505  sylow1lem2  19617  sylow3lem1  19645  efginvrel1  19746  frgpup3lem  19795  frgpup3  19796  prdscmnd  19879  iscyggen  19898  gsumval3  19925  gsumcllem  19926  gsumzsplit  19945  gsumsub  19966  gsummptf1o  19981  gsum2d  19990  gsum2d2  19992  gsumxp  19994  prdsgsum  19999  telgsumfz  20008  telgsumfz0  20010  telgsum  20012  dprdfsub  20041  dprdfeq0  20042  dprddisj2  20059  dprd2d2  20064  dpjidcl  20078  ablfaclem2  20106  ablfac2  20109  prdsmgp  20148  prdsrngd  20173  srgbinomlem3  20225  srgbinomlem4  20226  srgbinomlem  20227  gsumdixp  20316  prdsringd  20318  prdslmodd  20967  mulgrhm2  21489  frgpcyg  21592  freshmansdream  21593  evpmodpmf1o  21614  phlpropd  21673  frlmphl  21801  uvcresum  21813  frlmup1  21818  asclpropd  21917  psrass1lem  21952  psrlinv  21975  psrass1  21984  psrdi  21985  psrdir  21986  psrass23l  21987  psrcom  21988  psrass23  21989  resspsrmul  21996  mplsubrglem  22024  mplmonmul  22054  mplcoe1  22055  mplcoe5  22058  mplcoe4  22095  evlslem3  22104  evlslem1  22106  mhpmulcl  22153  psdmplcl  22166  psdadd  22167  psdmul  22170  psdmvr  22173  psrplusgpropd  22237  psropprmul  22239  coe1mul2  22272  coe1tm  22276  coe1tmmul2  22279  coe1tmmul  22280  coe1pwmul  22282  cply1mul  22300  ply1coe  22302  eqcoe1ply1eq  22303  lply1binomsc  22315  evl1gsummon  22369  evls1fpws  22373  rhmcomulmpl  22386  mamures  22401  grpvrinv  22403  mamuass  22406  mamudi  22407  mamudir  22408  mamuvs1  22409  mamuvs2  22410  mpomatmul  22452  mamutpos  22464  madetsumid  22467  dmatmul  22503  scmatscm  22519  1mavmul  22554  mavmulass  22555  mvmumamul1  22560  mulmarep1gsum1  22579  mulmarep1gsum2  22580  mdetleib2  22594  mdetfval1  22596  mdet0pr  22598  mdetdiag  22605  mdetdiagid  22606  mdetrlin  22608  mdetrsca  22609  mdetralt  22614  mdetunilem9  22626  gsummatr01  22665  smadiadetlem1a  22669  smadiadetlem3  22674  smadiadetlem4  22675  cpmatmcllem  22724  mat2pmatmul  22737  decpmatmullem  22777  decpmatmul  22778  pmatcollpw1lem2  22781  pmatcollpw  22787  pmatcollpw3lem  22789  pmatcollpwscmat  22797  idpm2idmp  22807  mp2pm2mplem3  22814  mp2pm2mplem4  22815  mp2pm2mplem5  22816  mp2pm2mp  22817  pm2mpghm  22822  pm2mpmhmlem2  22825  monmat2matmon  22830  pm2mp  22831  chpdmat  22847  chpscmat  22848  chpscmatgsumbin  22850  chpscmatgsummon  22851  chp0mat  22852  chpidmat  22853  chfacfscmulgsum  22866  chfacfpmmulgsum  22870  chfacfpmmulgsum2  22871  cayhamlem1  22872  cpmidgsumm2pm  22875  cpmidpmat  22879  cpmadugsumlemB  22880  cpmadugsumlemC  22881  cpmadugsumlemF  22882  cpmadumatpoly  22889  cayhamlem3  22893  cayhamlem4  22894  cayleyhamilton0  22895  cayleyhamiltonALT  22897  neiptopnei  23140  neiptopreu  23141  ptcnplem  23629  cnmpt1t  23673  cnmpt12  23675  cnmptkp  23688  cnmptk1  23689  cnmpt1k  23690  cnmptkk  23691  cnmptk1p  23693  cnmpt2k  23696  qtopeu  23724  pt1hmeo  23814  ptunhmeo  23816  xkocnv  23822  xkohmeo  23823  flfcnp2  24015  cnmpt1plusg  24095  istgp2  24099  tmdmulg  24100  tgpmulg  24101  tmdgsum  24103  subgtgp  24113  symgtgp  24114  tgpconncomp  24121  prdstgpd  24133  tsmsmhm  24154  tsmsadd  24155  tsmssub  24157  tgptsmscls  24158  tsmssplit  24160  tsmsxplem1  24161  tsmsxplem2  24162  cnmpt1vsca  24202  tlmtgp  24204  ustuqtoplem  24248  utopsnneip  24257  ressprdsds  24381  metuval  24562  nmfval0  24603  tngnm  24672  nmoeq0  24757  idnghm  24764  cnmpt1ds  24864  fsumcn  24894  expcn  24896  divccn  24897  expcnOLD  24898  divccnOLD  24899  divccncf  24932  negcncf  24948  negcncfOLD  24949  copco  25051  pcopt  25055  pcopt2  25056  pcoass  25057  pi1xfrcnvlem  25089  cnmpt1ip  25281  rrxnm  25425  rrxds  25427  minveclem3b  25462  divcncf  25482  ovolctb  25525  ovoliunnul  25542  voliunlem3  25587  ovolfs2  25606  uniioombllem2  25618  vitalilem4  25646  vitalilem5  25647  ismbf  25663  mbfss  25681  mbfmulc2re  25683  mbfneg  25685  mbfpos  25686  mbfposb  25688  mbfadd  25696  mbfsub  25697  mbfmulc2  25698  mbfinf  25700  mbflimsup  25701  mbflimlem  25702  i1fpos  25741  i1fposd  25742  itg1climres  25749  mbfmul  25761  itg2mulc  25782  itg2i1fseq  25790  itg2cnlem1  25796  itg2cnlem2  25797  itgresr  25814  iblneg  25838  i1fibl  25843  itgitg1  25844  iblsub  25857  itgfsum  25862  itgmulc2lem1  25867  limcmpt  25918  limccnp  25926  limcco  25928  dvreslem  25944  dvres2lem  25945  dvidlem  25950  dvcnp2  25955  dvcnp2OLD  25956  dvaddbr  25974  dvmulbr  25975  dvmulbrOLD  25976  dvmulf  25980  dvcmulf  25982  dvcobr  25983  dvcobrOLD  25984  dvcof  25986  dvcjbr  25987  dvcj  25988  dvfre  25989  dvexp  25991  dvexp2  25992  dvrec  25993  dvmptcmul  26002  dvmptdivc  26003  dvmptneg  26004  dvmptsub  26005  dvmptre  26007  dvmptim  26008  dvrecg  26011  dvmptdiv  26012  dvmptfsum  26013  dvcnvlem  26014  dvcnv  26015  dvexp3  26016  dvef  26018  dvsincos  26019  dv11cn  26040  lhop2  26054  lhop  26055  ftc2  26085  itgparts  26088  itgsubstlem  26089  mdegfval  26101  mdegmullem  26117  ply1termlem  26242  plypow  26244  plyconst  26245  plyeq0lem  26249  plypf1  26251  plyaddlem1  26252  plymullem1  26253  coeeulem  26263  coeidlem  26276  plyco  26280  coeeq2  26281  0dgr  26284  0dgrb  26285  dgrcolem1  26313  dgrcolem2  26314  plycjlem  26316  dvply1  26325  dvply2g  26326  dvply2gOLD  26327  plydiveu  26340  plyremlem  26346  elqaalem3  26363  taylfval  26400  dvtaylp  26412  taylthlem1  26415  taylthlem2  26416  taylthlem2OLD  26417  ulmshft  26433  mtestbdd  26448  iblulm  26450  itgulm2  26452  pserulm  26465  psercn2  26466  psercn2OLD  26467  pserdvlem2  26472  pserdv  26473  pserdv2  26474  abelthlem1  26475  abelthlem3  26477  advlog  26696  advlogexp  26697  dvcxp1  26782  dvcxp2  26783  dvcncxp1  26785  sqrtcn  26793  loglesqrt  26804  dvatan  26978  atantayl2  26981  atantayl3  26982  leibpi  26985  rlimcnp2  27009  efrlim  27012  efrlimOLD  27013  dfef2  27014  cxp2lim  27020  divsqrtsumlem  27023  lgamgulmlem2  27073  lgamgulm2  27079  lgamcvglem  27083  gamcvg2lem  27102  ftalem7  27122  basellem9  27132  muinv  27236  logfacrlim  27268  logexprlim  27269  dchrmullid  27296  dchrinvcl  27297  lgseisenlem3  27421  lgseisenlem4  27422  chtppilimlem2  27518  chebbnd2  27521  chpchtlim  27523  chpo1ub  27524  rpvmasumlem  27531  dchrmusumlema  27537  dchrvmasumlem1  27539  dchrvmasumiflem2  27546  dchrisum0fno1  27555  rpvmasum2  27556  dchrisum0lema  27558  dchrisum0lem1  27560  dchrisum0lem2a  27561  dchrisum0lem2  27562  dchrisum0  27564  dchrmusumlem  27566  dchrvmasumlem  27567  rpvmasum  27570  rplogsum  27571  logdivsum  27577  mulog2sumlem3  27580  vmalogdivsum2  27582  vmalogdivsum  27583  2vmadivsumlem  27584  logsqvma2  27587  log2sumbnd  27588  selberglem2  27590  selberg3lem1  27601  selberg3  27603  selberg4lem1  27604  selberg4  27605  pntrsumo1  27609  selberg3r  27613  selberg4r  27614  selberg34r  27615  pntrlog2bndlem2  27622  pntrlog2bndlem4  27624  pntrlog2bndlem5  27625  pntrlog2bndlem6  27627  padicabvf  27675  padicabvcxp  27676  mirval  28663  crctcshlem4  29840  clwlknf1oclwwlkn  30103  eucrct2eupth  30264  chscllem4  31659  brafnmul  31970  kbmul  31974  cofmpt2  32644  ofresid  32652  ofoprabco  32674  fmptunsnop  32709  fcobijfs  32734  gsummpt2d  33052  gsummptres  33055  gsummptres2  33056  gsummptfsf1o  33057  gsumfs2d  33058  gsumpart  33060  gsumhashmul  33064  gsumwrd2dccat  33070  fzto1st1  33122  fzto1st  33123  elrgspnlem1  33246  elrgspnlem2  33247  elrgspnlem3  33248  elrgspnlem4  33249  elrgspnsubrunlem1  33251  elrgspnsubrunlem2  33252  qusbas2  33434  qusima  33436  elrspunidl  33456  elrspunsn  33457  rprmdvdsprod  33562  evl1deg1  33601  evl1deg2  33602  evl1deg3  33603  gsummoncoe1fzo  33618  lbsdiflsp0  33677  fedgmullem1  33680  fedgmullem2  33681  fldextrspunlsplem  33723  fldextrspunlsp  33724  mdetpmtr1  33822  mdetlap  33831  xrge0mulc1cn  33940  esumval  34047  esumsnf  34065  esumpcvgval  34079  esumcvg  34087  esumcvgsum  34089  esumsup  34090  ofcfeqd2  34102  meascnbl  34220  sitgval  34334  probmeasb  34432  cndprobprob  34440  dstfrvclim1  34480  ballotlemfval  34492  ballotlemsval  34511  ballotlemieq  34519  plymul02  34561  plymulx0  34562  plymulx  34563  signsplypnf  34565  signstfv  34578  signstfvn  34584  signstfvp  34586  itgexpif  34621  logdivsqrle  34665  ptpconn  35238  cvmliftlem6  35295  cvmliftphtlem  35322  cvmlift3lem5  35328  elmrsubrn  35525  msubfval  35529  msubco  35536  divcnvlin  35733  knoppcnlem9  36502  knoppcnlem10  36503  knoppcnlem11  36504  bj-finsumval0  37286  curf  37605  matunitlindflem1  37623  matunitlindflem2  37624  poimirlem3  37630  poimirlem15  37642  poimirlem16  37643  poimirlem17  37644  poimirlem19  37646  poimirlem20  37647  broucube  37661  ovoliunnfl  37669  voliunnfl  37671  volsupnfl  37672  mbfposadd  37674  itg2addnclem  37678  itg2addnclem3  37680  itg2addnc  37681  itgaddnclem2  37686  itgaddnc  37687  iblsubnc  37688  itgsubnc  37689  itgmulc2nclem1  37693  itgmulc2nclem2  37694  itgmulc2nc  37695  itgabsnc  37696  ftc1cnnclem  37698  ftc1anclem3  37702  ftc1anclem5  37704  ftc1anclem6  37705  ftc1anclem8  37707  ftc1anc  37708  ftc2nc  37709  areacirclem1  37715  areacirclem2  37716  areacirclem4  37718  areacirc  37720  upixp  37736  lcmineqlem8  42037  lcmineqlem12  42041  dvrelog2b  42067  dvrelogpow2b  42069  aks4d1p1p6  42074  aks4d1p1p5  42076  aks6d1c1  42117  aks6d1c5lem3  42138  sticksstones12a  42158  sticksstones12  42159  sticksstones19  42166  aks6d1c6lem1  42171  aks6d1c6lem4  42174  aks6d1c7lem3  42183  qsalrel  42281  pwsgprod  42554  rhmcomulpsr  42561  evlsvvval  42573  evlsevl  42581  selvvvval  42595  evlselv  42597  fsuppssindlem1  42601  fsuppssind  42603  mhphf  42607  mzpsubst  42759  mzprename  42760  mzpcompact2lem  42762  eldioph2  42773  rabdiophlem2  42813  mendlmod  43201  mendassa  43202  areaquad  43228  fsovcnvlem  44026  hashnzfzclim  44341  expgrowthi  44352  expgrowth  44354  uzmptshftfval  44365  dvradcnv2  44366  binomcxplemrat  44369  binomcxplemfrat  44370  binomcxplemradcnv  44371  binomcxplemdvbinom  44372  binomcxplemcvg  44373  binomcxplemdvsum  44374  binomcxplemnotnn0  44375  mulc1cncfg  45604  expcnfg  45606  fprodcnlem  45614  clim1fr1  45616  divcnvg  45642  sublimc  45667  reclimc  45668  divlimc  45671  limsupresico  45715  limsuppnfdlem  45716  limsupvaluz  45723  supcnvlimsupmpt  45756  liminfresico  45786  climliminflimsupd  45816  cncfmptssg  45886  negcncfg  45896  cncficcgt0  45903  fprodcncf  45915  fprodsubrecnncnvlem  45922  fprodaddrecnncnvlem  45924  dvsinax  45928  dvasinbx  45935  dvdivf  45937  ioodvbdlimc1lem2  45947  ioodvbdlimc2lem  45949  dvnmptdivc  45953  dvxpaek  45955  dvnxpaek  45957  dvnmul  45958  dvnprodlem2  45962  ibliccsinexp  45966  itgsinexplem1  45969  itgsinexp  45970  iblempty  45980  itgcoscmulx  45984  itgsincmulx  45989  itgioocnicc  45992  iblcncfioo  45993  itgsbtaddcnst  45997  volioofmpt  46009  volicofmpt  46012  stoweidlem4  46019  stirlinglem5  46093  dirkerval  46106  dirkertrigeq  46116  dirkeritg  46117  dirkercncflem2  46119  dirkercncflem4  46121  fourierdlem16  46138  fourierdlem18  46140  fourierdlem21  46143  fourierdlem22  46144  fourierdlem28  46150  fourierdlem39  46161  fourierdlem40  46162  fourierdlem41  46163  fourierdlem53  46174  fourierdlem56  46177  fourierdlem57  46178  fourierdlem60  46181  fourierdlem61  46182  fourierdlem68  46189  fourierdlem73  46194  fourierdlem74  46195  fourierdlem75  46196  fourierdlem76  46197  fourierdlem78  46199  fourierdlem81  46202  fourierdlem82  46203  fourierdlem83  46204  fourierdlem84  46205  fourierdlem85  46206  fourierdlem88  46209  fourierdlem90  46211  fourierdlem92  46213  fourierdlem93  46214  fourierdlem95  46216  fourierdlem97  46218  fourierdlem101  46222  fourierdlem103  46224  fourierdlem104  46225  fourierdlem111  46232  fourierdlem112  46233  sqwvfoura  46243  sqwvfourb  46244  fouriersw  46246  elaa2lem  46248  etransclem4  46253  etransclem17  46266  etransclem18  46267  etransclem32  46281  etransclem46  46295  sge0z  46390  sge0revalmpt  46393  sge0tsms  46395  sge0sup  46406  sge0iunmptlemre  46430  sge0iun  46434  sge0xaddlem2  46449  ismeannd  46482  psmeasurelem  46485  meaiuninclem  46495  meaiininclem  46501  caratheodory  46543  isomenndlem  46545  ovnval  46556  hoicvrrex  46571  ovnlecvr  46573  ovncvrrp  46579  ovn0lem  46580  ovnsubaddlem1  46585  hoidmv1lelem2  46607  hoidmv1le  46609  hoidmvlelem3  46612  ovnhoilem2  46617  ovnhoi  46618  ovnlecvr2  46625  ovncvr2  46626  hspmbllem2  46642  ovolval2lem  46658  ovolval3  46662  ovolval5lem1  46667  ovolval5lem2  46668  ovnovollem1  46671  ovnovollem2  46672  vonioolem1  46695  vonicclem1  46698  vonct  46708  smflim  46792  smfinflem  46832  smflimsuplem5  46839  smfliminflem  46845  cfsetsnfsetfv  47069  fundcmpsurbijinjpreimafv  47394  fundcmpsurinjimaid  47398  fdmdifeqresdif  48258  ply1mulgsumlem2  48304  lincvalsc0  48338  linc0scn0  48340  lincdifsn  48341  lincsum  48346  lincscm  48347  lindslinindimp2lem4  48378  lindslinindsimp2lem5  48379  lincresunit3lem2  48397  1arymaptfo  48564  itcovalpclem1  48591  itcovalpclem2  48592  itcovalt2lem1  48596  itcovalt2lem2  48597  tposcurf1  48999  tposcurf2  49000  diag1  49004  fuco22  49034  fucocolem2  49049  fucocolem3  49050  fucocolem4  49051  fucoco  49052  fucolid  49056  fucorid  49057  postcofval  49059  precofval  49062  precofvalALT  49063  precofval2  49064  aacllem  49320  amgmwlem  49321