Theorem mpteq2dva 5188

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 2734	. 2 ⊢ (𝜑 → 𝐴 = 𝐴)
2		mpteq2dva.1	. 2 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 = 𝐶)
3	1, 2	mpteq12dva 5181	1 ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵) = (𝑥 ∈ 𝐴 ↦ 𝐶))

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

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 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-sb 2068  df-clab 2712  df-cleq 2725  df-clel 2808  df-opab 5158  df-mpt 5177

This theorem is referenced by:  mpteq2dv  5189  mpteq2ia  5190  2fvcoidd  7239  offval  7627  offval2  7638  coof  7642  caofinvl  7650  caofcom  7655  caofass  7658  caofdi  7660  caofdir  7661  caonncan  7662  curry1  8042  curry2  8045  mpocurryd  8207  pw2f1olem  9003  mapxpen  9065  xpmapenlem  9066  cantnfp1  9580  cantnflem1d  9587  cantnflem1  9588  cnfcom2lem  9600  dfac12lem1  10044  seqof  13970  seqof2  13971  swrdswrd  14616  repswswrd  14695  repswrevw  14698  revco  14745  ccatco  14746  repsco  14751  ofccat  14880  lo1eq  15479  rlimeq  15480  lo1mul2  15540  o1dif  15541  lo1sub  15542  rlimdiv  15557  caucvgr  15587  sumeq1  15600  fsumrlim  15722  fsumo1  15723  climfsum  15731  geomulcvg  15787  vdwlem8  16904  prmgapprmo  16978  restid2  17338  pwsplusgval  17398  pwsmulrval  17399  pwsvscafval  17402  qusin  17452  xpsaddlem  17481  xpsvsca  17485  catidd  17590  fuclid  17880  fucrid  17881  fucass  17882  setcepi  17999  prf1st  18114  prf2nd  18115  1st2ndprf  18116  curfcl  18142  curfuncf  18148  diag2  18155  curf2ndf  18157  hof2val  18166  hofcllem  18168  hofcl  18169  yonedalem4a  18185  yonedalem4c  18187  yonedalem3b  18189  yonedainv  18191  yonffthlem  18192  prdssgrpd  18645  prdsidlem  18681  prdsmndd  18682  mhmvlin  18713  pwsco2mhm  18745  frmdup3lem  18778  frmdup3  18779  smndex1gid  18815  smndex1igid  18816  grpinvpropd  18932  prdsinvlem  18966  pwsinvg  18970  pwssub  18971  galactghm  19320  cayleylem1  19328  pmtrprfval  19403  sylow1lem2  19515  sylow3lem1  19543  efginvrel1  19644  frgpup3lem  19693  frgpup3  19694  prdscmnd  19777  iscyggen  19796  gsumval3  19823  gsumcllem  19824  gsumzsplit  19843  gsumsub  19864  gsummptf1o  19879  gsum2d  19888  gsum2d2  19890  gsumxp  19892  prdsgsum  19897  telgsumfz  19906  telgsumfz0  19908  telgsum  19910  dprdfsub  19939  dprdfeq0  19940  dprddisj2  19957  dprd2d2  19962  dpjidcl  19976  ablfaclem2  20004  ablfac2  20007  prdsmgp  20073  prdsrngd  20098  srgbinomlem3  20150  srgbinomlem4  20151  srgbinomlem  20152  gsumdixp  20241  prdsringd  20243  prdslmodd  20906  mulgrhm2  21419  frgpcyg  21514  freshmansdream  21515  evpmodpmf1o  21537  phlpropd  21596  frlmphl  21722  uvcresum  21734  frlmup1  21739  asclpropd  21838  psrass1lem  21873  psrlinv  21896  psrass1  21904  psrdi  21905  psrdir  21906  psrass23l  21907  psrcom  21908  psrass23  21909  resspsrmul  21916  mplsubrglem  21944  mplmonmul  21974  mplcoe1  21975  mplcoe5  21978  mplcoe4  22009  evlslem3  22018  evlslem1  22020  mhpmulcl  22067  psdmplcl  22080  psdadd  22081  psdmul  22084  psdmvr  22087  psrplusgpropd  22151  psropprmul  22153  coe1mul2  22186  coe1tm  22190  coe1tmmul2  22193  coe1tmmul  22194  coe1pwmul  22196  cply1mul  22214  ply1coe  22216  eqcoe1ply1eq  22217  lply1binomsc  22229  evl1gsummon  22283  evls1fpws  22287  rhmcomulmpl  22300  mamures  22315  grpvrinv  22317  mamuass  22320  mamudi  22321  mamudir  22322  mamuvs1  22323  mamuvs2  22324  mpomatmul  22364  mamutpos  22376  madetsumid  22379  dmatmul  22415  scmatscm  22431  1mavmul  22466  mavmulass  22467  mvmumamul1  22472  mulmarep1gsum1  22491  mulmarep1gsum2  22492  mdetleib2  22506  mdetfval1  22508  mdet0pr  22510  mdetdiag  22517  mdetdiagid  22518  mdetrlin  22520  mdetrsca  22521  mdetralt  22526  mdetunilem9  22538  gsummatr01  22577  smadiadetlem1a  22581  smadiadetlem3  22586  smadiadetlem4  22587  cpmatmcllem  22636  mat2pmatmul  22649  decpmatmullem  22689  decpmatmul  22690  pmatcollpw1lem2  22693  pmatcollpw  22699  pmatcollpw3lem  22701  pmatcollpwscmat  22709  idpm2idmp  22719  mp2pm2mplem3  22726  mp2pm2mplem4  22727  mp2pm2mplem5  22728  mp2pm2mp  22729  pm2mpghm  22734  pm2mpmhmlem2  22737  monmat2matmon  22742  pm2mp  22743  chpdmat  22759  chpscmat  22760  chpscmatgsumbin  22762  chpscmatgsummon  22763  chp0mat  22764  chpidmat  22765  chfacfscmulgsum  22778  chfacfpmmulgsum  22782  chfacfpmmulgsum2  22783  cayhamlem1  22784  cpmidgsumm2pm  22787  cpmidpmat  22791  cpmadugsumlemB  22792  cpmadugsumlemC  22793  cpmadugsumlemF  22794  cpmadumatpoly  22801  cayhamlem3  22805  cayhamlem4  22806  cayleyhamilton0  22807  cayleyhamiltonALT  22809  neiptopnei  23050  neiptopreu  23051  ptcnplem  23539  cnmpt1t  23583  cnmpt12  23585  cnmptkp  23598  cnmptk1  23599  cnmpt1k  23600  cnmptkk  23601  cnmptk1p  23603  cnmpt2k  23606  qtopeu  23634  pt1hmeo  23724  ptunhmeo  23726  xkocnv  23732  xkohmeo  23733  flfcnp2  23925  cnmpt1plusg  24005  istgp2  24009  tmdmulg  24010  tgpmulg  24011  tmdgsum  24013  subgtgp  24023  symgtgp  24024  tgpconncomp  24031  prdstgpd  24043  tsmsmhm  24064  tsmsadd  24065  tsmssub  24067  tgptsmscls  24068  tsmssplit  24070  tsmsxplem1  24071  tsmsxplem2  24072  cnmpt1vsca  24112  tlmtgp  24114  ustuqtoplem  24157  utopsnneip  24166  ressprdsds  24289  metuval  24467  nmfval0  24508  tngnm  24569  nmoeq0  24654  idnghm  24661  cnmpt1ds  24761  fsumcn  24791  expcn  24793  divccn  24794  expcnOLD  24795  divccnOLD  24796  divccncf  24829  negcncf  24845  negcncfOLD  24846  copco  24948  pcopt  24952  pcopt2  24953  pcoass  24954  pi1xfrcnvlem  24986  cnmpt1ip  25177  rrxnm  25321  rrxds  25323  minveclem3b  25358  divcncf  25378  ovolctb  25421  ovoliunnul  25438  voliunlem3  25483  ovolfs2  25502  uniioombllem2  25514  vitalilem4  25542  vitalilem5  25543  ismbf  25559  mbfss  25577  mbfmulc2re  25579  mbfneg  25581  mbfpos  25582  mbfposb  25584  mbfadd  25592  mbfsub  25593  mbfmulc2  25594  mbfinf  25596  mbflimsup  25597  mbflimlem  25598  i1fpos  25637  i1fposd  25638  itg1climres  25645  mbfmul  25657  itg2mulc  25678  itg2i1fseq  25686  itg2cnlem1  25692  itg2cnlem2  25693  itgresr  25710  iblneg  25734  i1fibl  25739  itgitg1  25740  iblsub  25753  itgfsum  25758  itgmulc2lem1  25763  limcmpt  25814  limccnp  25822  limcco  25824  dvreslem  25840  dvres2lem  25841  dvidlem  25846  dvcnp2  25851  dvcnp2OLD  25852  dvaddbr  25870  dvmulbr  25871  dvmulbrOLD  25872  dvmulf  25876  dvcmulf  25878  dvcobr  25879  dvcobrOLD  25880  dvcof  25882  dvcjbr  25883  dvcj  25884  dvfre  25885  dvexp  25887  dvexp2  25888  dvrec  25889  dvmptcmul  25898  dvmptdivc  25899  dvmptneg  25900  dvmptsub  25901  dvmptre  25903  dvmptim  25904  dvrecg  25907  dvmptdiv  25908  dvmptfsum  25909  dvcnvlem  25910  dvcnv  25911  dvexp3  25912  dvef  25914  dvsincos  25915  dv11cn  25936  lhop2  25950  lhop  25951  ftc2  25981  itgparts  25984  itgsubstlem  25985  mdegfval  25997  mdegmullem  26013  ply1termlem  26138  plypow  26140  plyconst  26141  plyeq0lem  26145  plypf1  26147  plyaddlem1  26148  plymullem1  26149  coeeulem  26159  coeidlem  26172  plyco  26176  coeeq2  26177  0dgr  26180  0dgrb  26181  dgrcolem1  26209  dgrcolem2  26210  plycjlem  26212  dvply1  26221  dvply2g  26222  dvply2gOLD  26223  plydiveu  26236  plyremlem  26242  elqaalem3  26259  taylfval  26296  dvtaylp  26308  taylthlem1  26311  taylthlem2  26312  taylthlem2OLD  26313  ulmshft  26329  mtestbdd  26344  iblulm  26346  itgulm2  26348  pserulm  26361  psercn2  26362  psercn2OLD  26363  pserdvlem2  26368  pserdv  26369  pserdv2  26370  abelthlem1  26371  abelthlem3  26373  advlog  26593  advlogexp  26594  dvcxp1  26679  dvcxp2  26680  dvcncxp1  26682  sqrtcn  26690  loglesqrt  26701  dvatan  26875  atantayl2  26878  atantayl3  26879  leibpi  26882  rlimcnp2  26906  efrlim  26909  efrlimOLD  26910  dfef2  26911  cxp2lim  26917  divsqrtsumlem  26920  lgamgulmlem2  26970  lgamgulm2  26976  lgamcvglem  26980  gamcvg2lem  26999  ftalem7  27019  basellem9  27029  muinv  27133  logfacrlim  27165  logexprlim  27166  dchrmullid  27193  dchrinvcl  27194  lgseisenlem3  27318  lgseisenlem4  27319  chtppilimlem2  27415  chebbnd2  27418  chpchtlim  27420  chpo1ub  27421  rpvmasumlem  27428  dchrmusumlema  27434  dchrvmasumlem1  27436  dchrvmasumiflem2  27443  dchrisum0fno1  27452  rpvmasum2  27453  dchrisum0lema  27455  dchrisum0lem1  27457  dchrisum0lem2a  27458  dchrisum0lem2  27459  dchrisum0  27461  dchrmusumlem  27463  dchrvmasumlem  27464  rpvmasum  27467  rplogsum  27468  logdivsum  27474  mulog2sumlem3  27477  vmalogdivsum2  27479  vmalogdivsum  27480  2vmadivsumlem  27481  logsqvma2  27484  log2sumbnd  27485  selberglem2  27487  selberg3lem1  27498  selberg3  27500  selberg4lem1  27501  selberg4  27502  pntrsumo1  27506  selberg3r  27510  selberg4r  27511  selberg34r  27512  pntrlog2bndlem2  27519  pntrlog2bndlem4  27521  pntrlog2bndlem5  27522  pntrlog2bndlem6  27524  padicabvf  27572  padicabvcxp  27573  mirval  28636  crctcshlem4  29802  clwlknf1oclwwlkn  30068  eucrct2eupth  30229  chscllem4  31624  brafnmul  31935  kbmul  31939  cofmpt2  32620  ofresid  32628  ofoprabco  32650  fmptunsnop  32687  fcobijfs  32710  fcobijfs2  32711  gsummpt2d  33038  gsummptres  33041  gsummptres2  33042  gsummptfsf1o  33043  gsumfs2d  33044  gsumpart  33046  gsumhashmul  33050  gsumwrd2dccat  33056  fzto1st1  33080  fzto1st  33081  elrgspnlem1  33218  elrgspnlem2  33219  elrgspnlem3  33220  elrgspnlem4  33221  elrgspnsubrunlem1  33223  elrgspnsubrunlem2  33224  qusbas2  33380  qusima  33382  elrspunidl  33402  elrspunsn  33403  rprmdvdsprod  33508  ressply1evls1  33537  evl1deg1  33548  evl1deg2  33549  evl1deg3  33550  gsummoncoe1fzo  33567  mplmulmvr  33592  mplvrpmga  33595  mplvrpmmhm  33596  mplvrpmrhm  33597  issply  33604  esplyfval3  33614  esplyind  33615  lbsdiflsp0  33662  fedgmullem1  33665  fedgmullem2  33666  fldextrspunlsplem  33709  fldextrspunlsp  33710  extdgfialglem2  33729  mdetpmtr1  33859  mdetlap  33868  xrge0mulc1cn  33977  esumval  34082  esumsnf  34100  esumpcvgval  34114  esumcvg  34122  esumcvgsum  34124  esumsup  34125  ofcfeqd2  34137  meascnbl  34255  sitgval  34368  probmeasb  34466  cndprobprob  34474  dstfrvclim1  34514  ballotlemfval  34526  ballotlemsval  34545  ballotlemieq  34553  plymul02  34582  plymulx0  34583  plymulx  34584  signsplypnf  34586  signstfv  34599  signstfvn  34605  signstfvp  34607  itgexpif  34642  logdivsqrle  34686  ptpconn  35300  cvmliftlem6  35357  cvmliftphtlem  35384  cvmlift3lem5  35390  elmrsubrn  35587  msubfval  35591  msubco  35598  divcnvlin  35800  knoppcnlem9  36568  knoppcnlem10  36569  knoppcnlem11  36570  bj-finsumval0  37352  curf  37661  matunitlindflem1  37679  matunitlindflem2  37680  poimirlem3  37686  poimirlem15  37698  poimirlem16  37699  poimirlem17  37700  poimirlem19  37702  poimirlem20  37703  broucube  37717  ovoliunnfl  37725  voliunnfl  37727  volsupnfl  37728  mbfposadd  37730  itg2addnclem  37734  itg2addnclem3  37736  itg2addnc  37737  itgaddnclem2  37742  itgaddnc  37743  iblsubnc  37744  itgsubnc  37745  itgmulc2nclem1  37749  itgmulc2nclem2  37750  itgmulc2nc  37751  itgabsnc  37752  ftc1cnnclem  37754  ftc1anclem3  37758  ftc1anclem5  37760  ftc1anclem6  37761  ftc1anclem8  37763  ftc1anc  37764  ftc2nc  37765  areacirclem1  37771  areacirclem2  37772  areacirclem4  37774  areacirc  37776  upixp  37792  lcmineqlem8  42152  lcmineqlem12  42156  dvrelog2b  42182  dvrelogpow2b  42184  aks4d1p1p6  42189  aks4d1p1p5  42191  aks6d1c1  42232  aks6d1c5lem3  42253  sticksstones12a  42273  sticksstones12  42274  sticksstones19  42281  aks6d1c6lem1  42286  aks6d1c6lem4  42289  aks6d1c7lem3  42298  qsalrel  42361  pwsgprod  42665  rhmcomulpsr  42672  evlsvvval  42684  evlsevl  42692  selvvvval  42706  evlselv  42708  fsuppssindlem1  42712  fsuppssind  42714  mhphf  42718  mzpsubst  42868  mzprename  42869  mzpcompact2lem  42871  eldioph2  42882  rabdiophlem2  42922  mendlmod  43309  mendassa  43310  areaquad  43336  fsovcnvlem  44133  hashnzfzclim  44442  expgrowthi  44453  expgrowth  44455  uzmptshftfval  44466  dvradcnv2  44467  binomcxplemrat  44470  binomcxplemfrat  44471  binomcxplemradcnv  44472  binomcxplemdvbinom  44473  binomcxplemcvg  44474  binomcxplemdvsum  44475  binomcxplemnotnn0  44476  mulc1cncfg  45716  expcnfg  45718  fprodcnlem  45726  clim1fr1  45728  divcnvg  45754  sublimc  45777  reclimc  45778  divlimc  45781  limsupresico  45825  limsuppnfdlem  45826  limsupvaluz  45833  supcnvlimsupmpt  45866  liminfresico  45896  climliminflimsupd  45926  cncfmptssg  45996  negcncfg  46006  cncficcgt0  46013  fprodcncf  46025  fprodsubrecnncnvlem  46032  fprodaddrecnncnvlem  46034  dvsinax  46038  dvasinbx  46045  dvdivf  46047  ioodvbdlimc1lem2  46057  ioodvbdlimc2lem  46059  dvnmptdivc  46063  dvxpaek  46065  dvnxpaek  46067  dvnmul  46068  dvnprodlem2  46072  ibliccsinexp  46076  itgsinexplem1  46079  itgsinexp  46080  iblempty  46090  itgcoscmulx  46094  itgsincmulx  46099  itgioocnicc  46102  iblcncfioo  46103  itgsbtaddcnst  46107  volioofmpt  46119  volicofmpt  46122  stoweidlem4  46129  stirlinglem5  46203  dirkerval  46216  dirkertrigeq  46226  dirkeritg  46227  dirkercncflem2  46229  dirkercncflem4  46231  fourierdlem16  46248  fourierdlem18  46250  fourierdlem21  46253  fourierdlem22  46254  fourierdlem28  46260  fourierdlem39  46271  fourierdlem40  46272  fourierdlem41  46273  fourierdlem53  46284  fourierdlem56  46287  fourierdlem57  46288  fourierdlem60  46291  fourierdlem61  46292  fourierdlem68  46299  fourierdlem73  46304  fourierdlem74  46305  fourierdlem75  46306  fourierdlem76  46307  fourierdlem78  46309  fourierdlem81  46312  fourierdlem82  46313  fourierdlem83  46314  fourierdlem84  46315  fourierdlem85  46316  fourierdlem88  46319  fourierdlem90  46321  fourierdlem92  46323  fourierdlem93  46324  fourierdlem95  46326  fourierdlem97  46328  fourierdlem101  46332  fourierdlem103  46334  fourierdlem104  46335  fourierdlem111  46342  fourierdlem112  46343  sqwvfoura  46353  sqwvfourb  46354  fouriersw  46356  elaa2lem  46358  etransclem4  46363  etransclem17  46376  etransclem18  46377  etransclem32  46391  etransclem46  46405  sge0z  46500  sge0revalmpt  46503  sge0tsms  46505  sge0sup  46516  sge0iunmptlemre  46540  sge0iun  46544  sge0xaddlem2  46559  ismeannd  46592  psmeasurelem  46595  meaiuninclem  46605  meaiininclem  46611  caratheodory  46653  isomenndlem  46655  ovnval  46666  hoicvrrex  46681  ovnlecvr  46683  ovncvrrp  46689  ovn0lem  46690  ovnsubaddlem1  46695  hoidmv1lelem2  46717  hoidmv1le  46719  hoidmvlelem3  46722  ovnhoilem2  46727  ovnhoi  46728  ovnlecvr2  46735  ovncvr2  46736  hspmbllem2  46752  ovolval2lem  46768  ovolval3  46772  ovolval5lem1  46777  ovolval5lem2  46778  ovnovollem1  46781  ovnovollem2  46782  vonioolem1  46805  vonicclem1  46808  vonct  46818  smflim  46902  smfinflem  46942  smflimsuplem5  46949  smfliminflem  46955  cfsetsnfsetfv  47184  fundcmpsurbijinjpreimafv  47534  fundcmpsurinjimaid  47538  fdmdifeqresdif  48469  ply1mulgsumlem2  48515  lincvalsc0  48549  linc0scn0  48551  lincdifsn  48552  lincsum  48557  lincscm  48558  lindslinindimp2lem4  48589  lindslinindsimp2lem5  48590  lincresunit3lem2  48608  1arymaptfo  48771  itcovalpclem1  48798  itcovalpclem2  48799  itcovalt2lem1  48803  itcovalt2lem2  48804  tposcurf1  49427  tposcurf2  49428  diag1  49432  fuco22  49467  fucocolem2  49482  fucocolem3  49483  fucocolem4  49484  fucoco  49485  fucolid  49489  fucorid  49490  postcofval  49492  precofval  49495  precofvalALT  49496  precofval2  49497  fucoppcco  49537  islmd  49793  iscmd  49794  aacllem  49929  amgmwlem  49930