Theorem mpteq2dva 5190

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

Syntax hints:   → wi 4   ∧ wa 399   = wceq 1559   ∈ wcel 2141   ↦ cmpt 5178

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-8 2143  ax-9 2151  ax-ext 2733

This theorem depends on definitions:  df-bi 209  df-an 400  df-ex 1799  df-sb 2090  df-clab 2740  df-cleq 2753  df-clel 2836  df-opab 5160  df-mpt 5179

This theorem is referenced by:  mpteq2dv  5191  mpteq2ia  5192  2fvcoidd  7275  offval  7663  offval2  7674  coof  7678  caofinvl  7686  caofcom  7691  caofass  7694  caofdi  7696  caofdir  7697  caonncan  7698  curry1  8076  curry2  8079  mpocurryd  8242  pw2f1olem  9046  mapxpen  9108  xpmapenlem  9109  cantnfp1  9629  cantnflem1d  9636  cantnflem1  9637  cnfcom2lem  9649  dfac12lem1  10093  seqof  14065  seqof2  14066  swrdswrd  14711  repswswrd  14790  repswrevw  14793  revco  14840  ccatco  14841  repsco  14846  ofccat  14975  lo1eq  15585  rlimeq  15586  lo1mul2  15646  o1dif  15647  lo1sub  15648  rlimdiv  15663  caucvgr  15693  sumeq1  15706  fsumrlim  15829  fsumo1  15830  climfsum  15838  geomulcvg  15896  vdwlem8  17014  prmgapprmo  17088  restid2  17449  pwsplusgval  17510  pwsmulrval  17511  pwsvscafval  17514  qusin  17564  xpsaddlem  17593  xpsvsca  17597  catidd  17702  fuclid  17992  fucrid  17993  fucass  17994  setcepi  18111  prf1st  18226  prf2nd  18227  1st2ndprf  18228  curfcl  18254  curfuncf  18260  diag2  18267  curf2ndf  18269  hof2val  18278  hofcllem  18280  hofcl  18281  yonedalem4a  18297  yonedalem4c  18299  yonedalem3b  18301  yonedainv  18303  yonffthlem  18304  prdssgrpd  18757  prdsidlem  18793  prdsmndd  18794  mhmvlin  18825  pwsco2mhm  18857  frmdup3lem  18890  frmdup3  18891  smndex1gid  18928  smndex1gidOLD  18929  smndex1igidOLD  18931  grpinvpropd  19047  prdsinvlem  19081  pwsinvg  19085  pwssub  19086  galactghm  19434  cayleylem1  19442  pmtrprfval  19517  sylow1lem2  19629  sylow3lem1  19657  efginvrel1  19758  frgpup3lem  19807  frgpup3  19808  prdscmnd  19891  iscyggen  19910  gsumval3  19937  gsumcllem  19938  gsumzsplit  19957  gsumsub  19978  gsummptf1o  19993  gsum2d  20002  gsum2d2  20004  gsumxp  20006  prdsgsum  20011  telgsumfz  20020  telgsumfz0  20022  telgsum  20024  dprdfsub  20053  dprdfeq0  20054  dprddisj2  20071  dprd2d2  20076  dpjidcl  20090  ablfaclem2  20118  ablfac2  20121  prdsmgp  20187  prdsrngd  20212  srgbinomlem3  20264  srgbinomlem4  20265  srgbinomlem  20266  gsumdixp  20353  prdsringd  20355  pwsgprod  20364  prdslmodd  21023  mulgrhm2  21517  frgpcyg  21612  freshmansdream  21613  evpmodpmf1o  21635  phlpropd  21694  frlmphl  21820  uvcresum  21832  frlmup1  21837  asclpropd  21936  psrass1lem  21972  psrlinv  21994  psrass1  22002  psrdi  22003  psrdir  22004  psrass23l  22005  psrcom  22006  psrass23  22007  resspsrmul  22014  mplsubrglem  22042  mplmonmul  22076  mplcoe1  22077  mplcoe5  22080  mplcoe4  22111  evlslem3  22120  evlslem1  22122  evlsvvval  22133  rhmcomulmpl  22164  evlsevl  22172  selvvvval  22182  mhpmulcl  22201  psdmplcl  22214  psdadd  22215  psdmul  22218  psdmvr  22221  psrplusgpropd  22284  psropprmul  22286  coe1mul2  22319  coe1tm  22323  coe1tmmul2  22326  coe1tmmul  22327  coe1pwmul  22329  cply1mul  22346  ply1coe  22348  eqcoe1ply1eq  22349  lply1binomsc  22361  evl1gsummon  22415  evls1fpws  22419  mamures  22444  grpvrinv  22446  mamuass  22449  mamudi  22450  mamudir  22451  mamuvs1  22452  mamuvs2  22453  mpomatmul  22493  mamutpos  22505  madetsumid  22508  dmatmul  22544  scmatscm  22560  1mavmul  22595  mavmulass  22596  mvmumamul1  22601  mulmarep1gsum1  22620  mulmarep1gsum2  22621  mdetleib2  22635  mdetfval1  22637  mdet0pr  22639  mdetdiag  22646  mdetdiagid  22647  mdetrlin  22649  mdetrsca  22650  mdetralt  22655  mdetunilem9  22667  gsummatr01  22706  smadiadetlem1a  22710  smadiadetlem3  22715  smadiadetlem4  22716  cpmatmcllem  22765  mat2pmatmul  22778  decpmatmullem  22818  decpmatmul  22819  pmatcollpw1lem2  22822  pmatcollpw  22828  pmatcollpw3lem  22830  pmatcollpwscmat  22838  idpm2idmp  22848  mp2pm2mplem3  22855  mp2pm2mplem4  22856  mp2pm2mplem5  22857  mp2pm2mp  22858  pm2mpghm  22863  pm2mpmhmlem2  22866  monmat2matmon  22871  pm2mp  22872  chpdmat  22888  chpscmat  22889  chpscmatgsumbin  22891  chpscmatgsummon  22892  chp0mat  22893  chpidmat  22894  chfacfscmulgsum  22907  chfacfpmmulgsum  22911  chfacfpmmulgsum2  22912  cayhamlem1  22913  cpmidgsumm2pm  22916  cpmidpmat  22920  cpmadugsumlemB  22921  cpmadugsumlemC  22922  cpmadugsumlemF  22923  cpmadumatpoly  22930  cayhamlem3  22934  cayhamlem4  22935  cayleyhamilton0  22936  cayleyhamiltonALT  22938  neiptopnei  23179  neiptopreu  23180  ptcnplem  23668  cnmpt1t  23712  cnmpt12  23714  cnmptkp  23727  cnmptk1  23728  cnmpt1k  23729  cnmptkk  23730  cnmptk1p  23732  cnmpt2k  23735  qtopeu  23763  pt1hmeo  23853  ptunhmeo  23855  xkocnv  23861  xkohmeo  23862  flfcnp2  24054  cnmpt1plusg  24134  istgp2  24138  tmdmulg  24139  tgpmulg  24140  tmdgsum  24142  subgtgp  24152  symgtgp  24153  tgpconncomp  24160  prdstgpd  24172  tsmsmhm  24193  tsmsadd  24194  tsmssub  24196  tgptsmscls  24197  tsmssplit  24199  tsmsxplem1  24200  tsmsxplem2  24201  cnmpt1vsca  24241  tlmtgp  24243  ustuqtoplem  24286  utopsnneip  24295  ressprdsds  24418  metuval  24596  nmfval0  24637  tngnm  24698  nmoeq0  24783  idnghm  24790  cnmpt1ds  24890  fsumcn  24919  expcn  24921  divccn  24922  divccncf  24955  negcncf  24971  copco  25067  pcopt  25071  pcopt2  25072  pcoass  25073  pi1xfrcnvlem  25105  cnmpt1ip  25296  rrxnm  25440  rrxds  25442  minveclem3b  25477  divcncf  25496  ovolctb  25539  ovoliunnul  25556  voliunlem3  25601  ovolfs2  25620  uniioombllem2  25632  vitalilem4  25660  vitalilem5  25661  ismbf  25677  mbfss  25695  mbfmulc2re  25697  mbfneg  25699  mbfpos  25700  mbfposb  25702  mbfadd  25710  mbfsub  25711  mbfmulc2  25712  mbfinf  25714  mbflimsup  25715  mbflimlem  25716  i1fpos  25755  i1fposd  25756  itg1climres  25763  mbfmul  25775  itg2mulc  25796  itg2i1fseq  25804  itg2cnlem1  25810  itg2cnlem2  25811  itgresr  25828  iblneg  25852  i1fibl  25857  itgitg1  25858  iblsub  25871  itgfsum  25876  itgmulc2lem1  25881  limcmpt  25932  limccnp  25940  limcco  25942  dvreslem  25958  dvres2lem  25959  dvidlem  25964  dvcnp2  25969  dvaddbr  25987  dvmulbr  25988  dvmulf  25992  dvcmulf  25994  dvcobr  25995  dvcof  25997  dvcjbr  25998  dvcj  25999  dvfre  26000  dvexp  26002  dvexp2  26003  dvrec  26004  dvmptcmul  26013  dvmptdivc  26014  dvmptneg  26015  dvmptsub  26016  dvmptre  26018  dvmptim  26019  dvrecg  26022  dvmptdiv  26023  dvmptfsum  26024  dvcnvlem  26025  dvcnv  26026  dvexp3  26027  dvef  26029  dvsincos  26030  dv11cn  26050  lhop2  26064  lhop  26065  ftc2  26093  itgparts  26096  itgsubstlem  26097  mdegfval  26109  mdegmullem  26125  ply1termlem  26250  plypow  26252  plyconst  26253  plyeq0lem  26257  plypf1  26259  plyaddlem1  26260  plymullem1  26261  coeeulem  26271  coeidlem  26284  plyco  26288  coeeq2  26289  0dgr  26292  0dgrb  26293  dgrcolem1  26320  dgrcolem2  26321  plycjlem  26323  plymul02  26331  plyn0mulidp  26332  plymulidp  26333  dvply1  26335  dvply2g  26336  plydiveu  26349  plyremlem  26355  elqaalem3  26372  taylfval  26409  dvtaylp  26420  taylthlem1  26423  taylthlem2  26424  ulmshft  26440  mtestbdd  26455  iblulm  26457  itgulm2  26459  pserulm  26472  psercn2  26473  pserdvlem2  26478  pserdv  26479  pserdv2  26480  abelthlem1  26481  abelthlem3  26483  advlog  26706  advlogexp  26707  dvcxp1  26792  dvcxp2  26793  dvcncxp1  26795  sqrtcn  26802  loglesqrt  26813  dvatan  26987  atantayl2  26990  atantayl3  26991  leibpi  26994  rlimcnp2  27018  efrlim  27021  dfef2  27022  cxp2lim  27028  divsqrtsumlem  27031  lgamgulmlem2  27081  lgamgulm2  27087  lgamcvglem  27091  gamcvg2lem  27110  ftalem7  27130  basellem9  27140  muinv  27244  logfacrlim  27275  logexprlim  27276  dchrmullid  27303  dchrinvcl  27304  lgseisenlem3  27428  lgseisenlem4  27429  chtppilimlem2  27525  chebbnd2  27528  chpchtlim  27530  chpo1ub  27531  rpvmasumlem  27538  dchrmusumlema  27544  dchrvmasumlem1  27546  dchrvmasumiflem2  27553  dchrisum0fno1  27562  rpvmasum2  27563  dchrisum0lema  27565  dchrisum0lem1  27567  dchrisum0lem2a  27568  dchrisum0lem2  27569  dchrisum0  27571  dchrmusumlem  27573  dchrvmasumlem  27574  rpvmasum  27577  rplogsum  27578  logdivsum  27584  mulog2sumlem3  27587  vmalogdivsum2  27589  vmalogdivsum  27590  2vmadivsumlem  27591  logsqvma2  27594  log2sumbnd  27595  selberglem2  27597  selberg3lem1  27608  selberg3  27610  selberg4lem1  27611  selberg4  27612  pntrsumo1  27616  selberg3r  27620  selberg4r  27621  selberg34r  27622  pntrlog2bndlem2  27629  pntrlog2bndlem4  27631  pntrlog2bndlem5  27632  pntrlog2bndlem6  27634  padicabvf  27682  padicabvcxp  27683  mirval  28811  crctcshlem4  29976  clwlknf1oclwwlkn  30242  eucrct2eupth  30403  chscllem4  31799  brafnmul  32110  kbmul  32114  cofmpt2  32796  ofresid  32804  ofoprabco  32826  fmptunsnop  32862  fcobijfs  32883  fcobijfs2  32884  gsummpt2d  33189  gsummptres  33192  gsummptres2  33193  gsummptf1od  33195  gsummptp1  33197  gsummptfsf1o  33200  gsumfs2d  33201  gsumpart  33203  gsumhashmul  33207  gsummulsubdishift1  33208  gsummulsubdishift2  33209  gsumwrd2dccat  33218  fzto1st1  33242  fzto1st  33243  elrgspnlem1  33383  elrgspnlem2  33384  elrgspnlem3  33385  elrgspnlem4  33386  elrgspnsubrunlem1  33388  elrgspnsubrunlem2  33389  qusbas2  33552  qusima  33554  elrspunidl  33574  elrspunsn  33575  rprmdvdsprod  33690  ressply1evls1  33721  evl1deg1  33732  evl1deg2  33733  evl1deg3  33734  gsummoncoe1fzo  33753  mplasclco  33773  selvply1rhmlemb  33776  selvply1rhmlem2  33778  selvply1rhmlem4  33780  selvply1rhm0  33783  mplmulmvr  33796  evlextv  33799  mplvrpmga  33802  mplvrpmmhm  33803  mplvrpmrhm  33804  psrgsum  33805  psrmonmul  33807  issply  33818  esplyfval0  33821  esplyfval3  33829  esplyfval1  33830  esplyfvaln  33831  esplyind  33832  vietalem  33836  lbsdiflsp0  33883  fedgmullem1  33886  fedgmullem2  33887  fldextrspunlsplem  33930  fldextrspunlsp  33931  extdgfialglem2  33950  mdetpmtr1  34080  mdetlap  34089  xrge0mulc1cn  34198  esumval  34303  esumsnf  34321  esumpcvgval  34335  esumcvg  34343  esumcvgsum  34345  esumsup  34346  ofcfeqd2  34358  meascnbl  34476  sitgval  34589  probmeasb  34687  cndprobprob  34695  dstfrvclim1  34735  ballotlemfval  34747  ballotlemsval  34766  ballotlemieq  34774  signsplypnf  34804  signstfv  34817  signstfvn  34823  signstfvp  34825  itgexpif  34860  logdivsqrle  34904  ptpconn  35543  cvmliftlem6  35600  cvmliftphtlem  35627  cvmlift3lem5  35633  elmrsubrn  35830  msubfval  35834  msubco  35841  divcnvlin  36043  knoppcnlem9  36899  knoppcnlem10  36900  knoppcnlem11  36901  bj-finsumval0  37737  curf  38057  matunitlindflem1  38075  matunitlindflem2  38076  poimirlem3  38082  poimirlem15  38094  poimirlem16  38095  poimirlem17  38096  poimirlem19  38098  poimirlem20  38099  broucube  38113  ovoliunnfl  38121  voliunnfl  38123  volsupnfl  38124  mbfposadd  38126  itg2addnclem  38130  itg2addnclem3  38132  itg2addnc  38133  itgaddnclem2  38138  itgaddnc  38139  iblsubnc  38140  itgsubnc  38141  itgmulc2nclem1  38145  itgmulc2nclem2  38146  itgmulc2nc  38147  itgabsnc  38148  ftc1cnnclem  38150  ftc1anclem3  38154  ftc1anclem5  38156  ftc1anclem6  38157  ftc1anclem8  38159  ftc1anc  38160  ftc2nc  38161  areacirclem1  38167  areacirclem2  38168  areacirclem4  38170  areacirc  38172  upixp  38188  lcmineqlem8  42613  lcmineqlem12  42617  dvrelog2b  42643  dvrelogpow2b  42645  aks4d1p1p6  42650  aks4d1p1p5  42652  aks6d1c1  42693  aks6d1c5lem3  42714  sticksstones12a  42734  sticksstones12  42735  sticksstones19  42742  aks6d1c6lem1  42747  aks6d1c6lem4  42750  aks6d1c7lem3  42759  qsalrel  42817  rhmcomulpsr  43124  evlselv  43131  fsuppssindlem1  43133  fsuppssind  43135  mhphf  43139  mzpsubst  43289  mzprename  43290  mzpcompact2lem  43292  eldioph2  43303  rabdiophlem2  43339  mendlmod  43726  mendassa  43727  areaquad  43753  fsovcnvlem  44549  hashnzfzclim  44858  expgrowthi  44869  expgrowth  44871  uzmptshftfval  44882  dvradcnv2  44883  binomcxplemrat  44886  binomcxplemfrat  44887  binomcxplemradcnv  44888  binomcxplemdvbinom  44889  binomcxplemcvg  44890  binomcxplemdvsum  44891  binomcxplemnotnn0  44892  mulc1cncfg  46125  expcnfg  46127  fprodcnlem  46135  clim1fr1  46137  divcnvg  46163  sublimc  46186  reclimc  46187  divlimc  46190  limsupresico  46234  limsuppnfdlem  46235  limsupvaluz  46242  supcnvlimsupmpt  46275  liminfresico  46305  climliminflimsupd  46335  cncfmptssg  46405  negcncfg  46415  cncficcgt0  46422  fprodcncf  46434  fprodsubrecnncnvlem  46441  fprodaddrecnncnvlem  46443  dvsinax  46447  dvasinbx  46454  dvdivf  46456  ioodvbdlimc1lem2  46466  ioodvbdlimc2lem  46468  dvnmptdivc  46472  dvxpaek  46474  dvnxpaek  46476  dvnmul  46477  dvnprodlem2  46481  ibliccsinexp  46485  itgsinexplem1  46488  itgsinexp  46489  iblempty  46499  itgcoscmulx  46503  itgsincmulx  46508  itgioocnicc  46511  iblcncfioo  46512  itgsbtaddcnst  46516  volioofmpt  46528  volicofmpt  46531  stoweidlem4  46538  stirlinglem5  46612  dirkerval  46625  dirkertrigeq  46635  dirkeritg  46636  dirkercncflem2  46638  dirkercncflem4  46640  fourierdlem16  46657  fourierdlem18  46659  fourierdlem21  46662  fourierdlem22  46663  fourierdlem28  46669  fourierdlem39  46680  fourierdlem40  46681  fourierdlem41  46682  fourierdlem53  46693  fourierdlem56  46696  fourierdlem57  46697  fourierdlem60  46700  fourierdlem61  46701  fourierdlem68  46708  fourierdlem73  46713  fourierdlem74  46714  fourierdlem75  46715  fourierdlem76  46716  fourierdlem78  46718  fourierdlem81  46721  fourierdlem82  46722  fourierdlem83  46723  fourierdlem84  46724  fourierdlem85  46725  fourierdlem88  46728  fourierdlem90  46730  fourierdlem92  46732  fourierdlem93  46733  fourierdlem95  46735  fourierdlem97  46737  fourierdlem101  46741  fourierdlem103  46743  fourierdlem104  46744  fourierdlem111  46751  fourierdlem112  46752  sqwvfoura  46762  sqwvfourb  46763  fouriersw  46765  elaa2lem  46767  etransclem4  46772  etransclem17  46785  etransclem18  46786  etransclem32  46800  etransclem46  46814  sge0z  46909  sge0revalmpt  46912  sge0tsms  46914  sge0sup  46925  sge0iunmptlemre  46949  sge0iun  46953  sge0xaddlem2  46968  ismeannd  47001  psmeasurelem  47004  meaiuninclem  47014  meaiininclem  47020  caratheodory  47062  isomenndlem  47064  ovnval  47075  hoicvrrex  47090  ovnlecvr  47092  ovncvrrp  47098  ovn0lem  47099  ovnsubaddlem1  47104  hoidmv1lelem2  47126  hoidmv1le  47128  hoidmvlelem3  47131  ovnhoilem2  47136  ovnhoi  47137  ovnlecvr2  47144  ovncvr2  47145  hspmbllem2  47161  ovolval2lem  47177  ovolval3  47181  ovolval5lem1  47186  ovolval5lem2  47187  ovnovollem1  47190  ovnovollem2  47191  vonioolem1  47214  vonicclem1  47217  vonct  47227  smflim  47311  smfinflem  47351  smflimsuplem5  47358  smfliminflem  47364  cfsetsnfsetfv  47611  fundcmpsurbijinjpreimafv  47973  fundcmpsurinjimaid  47977  fdmdifeqresdif  48924  ply1mulgsumlem2  48969  lincvalsc0  49003  linc0scn0  49005  lincdifsn  49006  lincsum  49011  lincscm  49012  lindslinindimp2lem4  49043  lindslinindsimp2lem5  49044  lincresunit3lem2  49062  1arymaptfo  49225  itcovalpclem1  49252  itcovalpclem2  49253  itcovalt2lem1  49257  itcovalt2lem2  49258  tposcurf1  49880  tposcurf2  49881  diag1  49885  fuco22  49920  fucocolem2  49935  fucocolem3  49936  fucocolem4  49937  fucoco  49938  fucolid  49942  fucorid  49943  postcofval  49945  precofval  49948  precofvalALT  49949  precofval2  49950  fucoppcco  49990  islmd  50246  iscmd  50247  aacllem  50382  amgmwlem  50383