Theorem mpteq2dva 5197

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   = wceq 1569   ∈ wcel 2144   ↦ cmpt 5185

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-opab 5167  df-mpt 5186

This theorem is used by:  mpteq2dv  5198  mpteq2ia  5199  2fvcoidd  7306  offval  7703  offval2  7714  coof  7718  caofinvl  7726  caofcom  7731  caofass  7734  caofdi  7736  caofdir  7737  caonncan  7738  curry1  8118  curry2  8121  mpocurryd  8290  curf  8894  pw2f1olem  9104  mapxpen  9166  xpmapenlem  9167  cantnfp1  9686  cantnflem1d  9693  cantnflem1  9694  cnfcom2lem  9706  dfac12lem1  10226  seqof  14206  seqof2  14207  swrdswrd  14859  repswswrd  14940  repswrevw  14943  revco  14990  ccatco  14991  repsco  14996  ofccat  15128  lo1eq  15741  rlimeq  15742  lo1mul2  15802  o1dif  15803  lo1sub  15804  rlimdiv  15819  caucvgr  15849  sumeq1  15862  fsumrlim  15984  fsumo1  15985  climfsum  15993  geomulcvg  16051  vdwlem8  17172  prmgapprmo  17246  restid2  17607  pwsplusgval  17668  pwsmulrval  17669  pwsvscafval  17672  qusin  17722  xpsaddlem  17751  xpsvsca  17755  catidd  17860  fuclid  18150  fucrid  18151  fucass  18152  setcepi  18269  prf1st  18384  prf2nd  18385  1st2ndprf  18386  curfcl  18412  curfuncf  18418  diag2  18425  curf2ndf  18427  hof2val  18436  hofcllem  18438  hofcl  18439  yonedalem4a  18455  yonedalem4c  18457  yonedalem3b  18459  yonedainv  18461  yonffthlem  18462  prdssgrpd  18928  prdsidlem  18969  prdsmndd  18970  mhmvlin  19002  pwsco2mhm  19035  frmdup3lem  19068  frmdup3  19069  smndex1gid  19106  smndex1gidOLD  19107  smndex1igidOLD  19109  grpinvpropd  19231  prdsinvlem  19265  pwsinvg  19269  pwssub  19270  galactghm  19624  cayleylem1  19632  pmtrprfval  19707  sylow1lem2  19819  sylow3lem1  19847  efginvrel1  19948  frgpup3lem  19997  frgpup3  19998  prdscmnd  20081  iscyggen  20100  gsumval3  20127  gsumcllem  20128  gsumzsplit  20147  gsumsub  20168  gsummptf1o  20183  gsum2d  20192  gsum2d2  20194  gsumxp  20196  prdsgsum  20201  telgsumfz  20210  telgsumfz0  20212  telgsum  20214  dprdfsub  20243  dprdfeq0  20244  dprddisj2  20261  dprd2d2  20266  dpjidcl  20280  ablfaclem2  20308  ablfac2  20311  prdsmgp  20377  prdsrngd  20404  srgbinomlem3  20460  srgbinomlem4  20461  srgbinomlem  20462  gsumdixp  20554  prdsringd  20556  pwsgprod  20565  prdslmodd  21250  mulgrhm2  21790  frgpcyg  21885  freshmansdream  21886  evpmodpmf1o  21908  phlpropd  21967  frlmphl  22093  uvcresum  22105  frlmup1  22110  asclpropd  22211  psrass1lem  22247  psrlinv  22269  psrass1  22277  psrdi  22278  psrdir  22279  psrass23l  22280  psrcom  22281  psrass23  22282  resspsrmul  22289  mplsubrglem  22317  mplmonmul  22351  mplcoe1  22352  mplcoe5  22355  mplcoe4  22386  evlslem3  22395  evlslem1  22397  evlsvvval  22408  rhmcomulmpl  22439  evlsevl  22447  selvvvval  22457  mhpmulcl  22476  psdmplcl  22489  psdadd  22490  psdmul  22493  psdmvr  22496  psrplusgpropd  22559  psropprmul  22561  coe1mul2  22594  coe1tm  22598  coe1tmmul2  22601  coe1tmmul  22602  coe1pwmul  22604  cply1mul  22620  ply1coe  22622  eqcoe1ply1eq  22623  lply1binomsc  22635  evl1gsummon  22689  evls1fpws  22693  mamures  22718  grpvrinv  22720  mamuass  22723  mamudi  22724  mamudir  22725  mamuvs1  22726  mamuvs2  22727  mpomatmul  22767  mamutpos  22779  madetsumid  22782  dmatmul  22818  scmatscm  22834  1mavmul  22869  mavmulass  22870  mvmumamul1  22875  mulmarep1gsum1  22894  mulmarep1gsum2  22895  mdetleib2  22909  mdetfval1  22911  mdet0pr  22913  mdetdiag  22920  mdetdiagid  22921  mdetrlin  22923  mdetrsca  22924  mdetralt  22929  mdetunilem9  22941  gsummatr01  22980  smadiadetlem1a  22984  smadiadetlem3  22989  smadiadetlem4  22990  matunitlindflem1  23000  matunitlindflem2  23001  cpmatmcllem  23042  mat2pmatmul  23055  decpmatmullem  23095  decpmatmul  23096  pmatcollpw1lem2  23099  pmatcollpw  23105  pmatcollpw3lem  23107  pmatcollpwscmat  23115  idpm2idmp  23125  mp2pm2mplem3  23132  mp2pm2mplem4  23133  mp2pm2mplem5  23134  mp2pm2mp  23135  pm2mpghm  23140  pm2mpmhmlem2  23143  monmat2matmon  23148  pm2mp  23149  chpdmat  23165  chpscmat  23166  chpscmatgsumbin  23168  chpscmatgsummon  23169  chp0mat  23170  chpidmat  23171  chfacfscmulgsum  23184  chfacfpmmulgsum  23188  chfacfpmmulgsum2  23189  cayhamlem1  23190  cpmidgsumm2pm  23193  cpmidpmat  23197  cpmadugsumlemB  23198  cpmadugsumlemC  23199  cpmadugsumlemF  23200  cpmadumatpoly  23207  cayhamlem3  23211  cayhamlem4  23212  cayleyhamilton0  23213  cayleyhamiltonALT  23215  neiptopnei  23456  neiptopreu  23457  ptcnplem  23946  cnmpt1t  23990  cnmpt12  23992  cnmptkp  24005  cnmptk1  24006  cnmpt1k  24007  cnmptkk  24008  cnmptk1p  24010  cnmpt2k  24013  qtopeu  24041  pt1hmeo  24131  ptunhmeo  24133  xkocnv  24139  xkohmeo  24140  flfcnp2  24332  cnmpt1plusg  24412  istgp2  24416  tmdmulg  24417  tgpmulg  24418  tmdgsum  24420  subgtgp  24430  symgtgp  24431  tgpconncomp  24438  prdstgpd  24450  tsmsmhm  24471  tsmsadd  24472  tsmssub  24474  tgptsmscls  24475  tsmssplit  24477  tsmsxplem1  24478  tsmsxplem2  24479  cnmpt1vsca  24519  tlmtgp  24521  ustuqtoplem  24564  utopsnneip  24573  ressprdsds  24696  metuval  24874  nmfval0  24915  tngnm  24976  nmoeq0  25061  idnghm  25068  cnmpt1ds  25168  fsumcn  25197  expcn  25199  divccn  25200  divccncf  25233  negcncf  25249  copco  25345  pcopt  25349  pcopt2  25350  pcoass  25351  pi1xfrcnvlem  25383  cnmpt1ip  25574  rrxnm  25718  rrxds  25720  minveclem3b  25755  divcncf  25774  ovolctb  25817  ovoliunnul  25834  voliunlem3  25879  ovolfs2  25898  uniioombllem2  25910  vitalilem4  25938  vitalilem5  25939  ismbf  25955  mbfss  25973  mbfmulc2re  25975  mbfneg  25977  mbfpos  25978  mbfposb  25980  mbfadd  25988  mbfsub  25989  mbfmulc2  25990  mbfinf  25992  mbflimsup  25993  mbflimlem  25994  i1fpos  26033  i1fposd  26034  itg1climres  26041  mbfmul  26053  itg2mulc  26074  itg2i1fseq  26082  itg2cnlem1  26088  itg2cnlem2  26089  itgresr  26105  iblneg  26129  i1fibl  26134  itgitg1  26135  iblsub  26148  itgfsum  26153  itgmulc2lem1  26158  limcmpt  26209  limccnp  26217  limcco  26219  dvreslem  26235  dvres2lem  26236  dvidlem  26241  dvcnp2  26246  dvaddbr  26264  dvmulbr  26265  dvmulf  26269  dvcmulf  26271  dvcobr  26272  dvcof  26274  dvcjbr  26275  dvcj  26276  dvfre  26277  dvexp  26279  dvexp2  26280  dvrec  26281  dvmptcmul  26290  dvmptdivc  26291  dvmptneg  26292  dvmptsub  26293  dvmptre  26295  dvmptim  26296  dvrecg  26299  dvmptdiv  26300  dvmptfsum  26301  dvcnvlem  26302  dvcnv  26303  dvexp3  26304  dvef  26306  dvsincos  26307  dv11cn  26327  lhop2  26341  lhop  26342  ftc2  26370  itgparts  26373  itgsubstlem  26374  mdegfval  26386  mdegmullem  26402  ply1termlem  26527  plypow  26529  plyconst  26530  plyeq0lem  26535  plypf1  26537  plyaddlem1  26538  plymullem1  26539  coeeulem  26549  coeidlem  26562  plyco  26566  coeeq2  26567  0dgr  26570  0dgrb  26571  dgrcolem1  26598  dgrcolem2  26599  plycjlem  26601  plymul02  26607  plyn0mulidp  26608  plymulidp  26609  dvply1  26611  dvply2g  26612  plydiveu  26625  plyremlem  26631  elqaalem3  26650  taylfval  26692  dvtaylp  26703  taylthlem1  26706  taylthlem2  26707  ulmshft  26723  mtestbdd  26738  iblulm  26740  itgulm2  26742  pserulm  26755  psercn2  26756  pserdvlem2  26761  pserdv  26762  pserdv2  26763  abelthlem1  26764  abelthlem3  26766  advlog  26988  advlogexp  26989  dvcxp1  27074  dvcxp2  27075  dvcncxp1  27077  sqrtcn  27084  loglesqrt  27095  dvatan  27269  atantayl2  27272  atantayl3  27273  leibpi  27276  rlimcnp2  27300  efrlim  27303  dfef2  27304  cxp2lim  27310  divsqrtsumlem  27313  lgamgulmlem2  27363  lgamgulm2  27369  lgamcvglem  27373  gamcvg2lem  27392  ftalem7  27412  basellem9  27422  muinv  27526  logfacrlim  27557  logexprlim  27558  dchrmullid  27585  dchrinvcl  27586  lgseisenlem3  27710  lgseisenlem4  27711  chtppilimlem2  27807  chebbnd2  27810  chpchtlim  27812  chpo1ub  27813  rpvmasumlem  27820  dchrmusumlema  27826  dchrvmasumlem1  27828  dchrvmasumiflem2  27835  dchrisum0fno1  27844  rpvmasum2  27845  dchrisum0lema  27847  dchrisum0lem1  27849  dchrisum0lem2a  27850  dchrisum0lem2  27851  dchrisum0  27853  dchrmusumlem  27855  dchrvmasumlem  27856  rpvmasum  27859  rplogsum  27860  logdivsum  27866  mulog2sumlem3  27869  vmalogdivsum2  27871  vmalogdivsum  27872  2vmadivsumlem  27873  logsqvma2  27876  log2sumbnd  27877  selberglem2  27879  selberg3lem1  27890  selberg3  27892  selberg4lem1  27893  selberg4  27894  pntrsumo1  27898  selberg3r  27902  selberg4r  27903  selberg34r  27904  pntrlog2bndlem2  27911  pntrlog2bndlem4  27913  pntrlog2bndlem5  27914  pntrlog2bndlem6  27916  padicabvf  27964  padicabvcxp  27965  mirval  29133  crctcshlem4  30415  clwlknf1oclwwlkn  30681  eucrct2eupth  30852  chscllem4  32248  brafnmul  32559  kbmul  32563  cofmpt2  33276  ofresid  33284  ofoprabco  33306  fmptunsnop  33341  fcobijfs  33360  fcobijfs2  33361  gsummpt2d  33657  gsummptres  33660  gsummptres2  33661  gsummptf1od  33663  gsummptp1  33665  gsummptfsf1o  33668  gsumfs2d  33669  gsumpart  33671  gsumhashmul  33675  gsummulsubdishift1  33676  gsummulsubdishift2  33677  gsumwrd2dccat  33686  fzto1st1  33710  fzto1st  33711  elrgspnlem1  33850  elrgspnlem2  33851  elrgspnlem3  33852  elrgspnlem4  33853  elrgspnsubrunlem1  33855  elrgspnsubrunlem2  33856  qusbas2  34004  qusima  34006  elrspunidl  34025  elrspunsn  34026  rprmdvdsprod  34113  ressply1evls1  34144  evl1deg1  34155  evl1deg2  34156  evl1deg3  34157  gsummoncoe1fzo  34176  mplasclco  34195  selvply1rhmlemb  34198  selvply1rhmlem2  34200  selvply1rhmlem4  34202  selvply1rhm0  34205  mplmulmvr  34218  evlextv  34221  mplvrpmga  34224  mplvrpmmhm  34225  mplvrpmrhm  34226  psrgsum  34227  psrmonmul  34229  issply  34240  esplyfval0  34243  esplyfval3  34251  esplyfval1  34252  esplyfvaln  34253  esplyind  34254  vietalem  34258  lbsdiflsp0  34305  fedgmullem1  34308  fedgmullem2  34309  fldextrspunlsplem  34352  fldextrspunlsp  34353  extdgfialglem2  34372  mdetpmtr1  34502  mdetlap  34511  xrge0mulc1cn  34620  esumval  34725  esumsnf  34743  esumpcvgval  34757  esumcvg  34765  esumcvgsum  34767  esumsup  34768  ofcfeqd2  34780  meascnbl  34899  sitgval  35011  probmeasb  35109  cndprobprob  35117  dstfrvclim1  35157  ballotlemfval  35169  ballotlemsval  35188  ballotlemieq  35196  signsplypnf  35226  signstfv  35239  signstfvn  35245  signstfvp  35247  itgexpif  35282  logdivsqrle  35326  ptpconn  36085  cvmliftlem6  36142  cvmliftphtlem  36169  cvmlift3lem5  36175  elmrsubrn  36372  msubfval  36376  msubco  36383  divcnvlin  36591  knoppcnlem9  37460  knoppcnlem10  37461  knoppcnlem11  37462  bj-finsumval0  38300  poimirlem3  38635  poimirlem15  38647  poimirlem16  38648  poimirlem17  38649  poimirlem19  38651  poimirlem20  38652  broucube  38666  ovoliunnfl  38674  voliunnfl  38676  volsupnfl  38677  mbfposadd  38679  itg2addnclem  38683  itg2addnclem3  38685  itg2addnc  38686  itgaddnclem2  38691  itgaddnc  38692  iblsubnc  38693  itgsubnc  38694  itgmulc2nclem1  38698  itgmulc2nclem2  38699  itgmulc2nc  38700  itgabsnc  38701  ftc1cnnclem  38703  ftc1anclem3  38707  ftc1anclem5  38709  ftc1anclem6  38710  ftc1anclem8  38712  ftc1anc  38713  ftc2nc  38714  areacirclem1  38720  areacirclem2  38721  areacirclem4  38723  areacirc  38725  upixp  38757  lcmineqlem8  43180  lcmineqlem12  43184  dvrelog2b  43210  dvrelogpow2b  43212  aks4d1p1p6  43217  aks4d1p1p5  43219  aks6d1c1  43260  aks6d1c5lem3  43281  sticksstones12a  43301  sticksstones12  43302  sticksstones19  43309  aks6d1c6lem1  43314  aks6d1c6lem4  43317  aks6d1c7lem3  43326  qsalrel  43386  rhmcomulpsr  43704  evlselv  43711  fsuppssindlem1  43713  fsuppssind  43715  mhphf  43719  mzpsubst  43853  mzprename  43854  mzpcompact2lem  43856  eldioph2  43867  rabdiophlem2  43903  mendlmod  44285  mendassa  44286  areaquad  44312  fsovcnvlem  45107  hashnzfzclim  45400  expgrowthi  45411  expgrowth  45413  uzmptshftfval  45424  dvradcnv2  45425  binomcxplemrat  45428  binomcxplemfrat  45429  binomcxplemradcnv  45430  binomcxplemdvbinom  45431  binomcxplemcvg  45432  binomcxplemdvsum  45433  binomcxplemnotnn0  45434  mulc1cncfg  46695  expcnfg  46697  fprodcnlem  46705  clim1fr1  46707  divcnvg  46733  sublimc  46756  reclimc  46757  divlimc  46760  limsupresico  46804  limsuppnfdlem  46805  limsupvaluz  46812  supcnvlimsupmpt  46845  liminfresico  46875  climliminflimsupd  46905  cncfmptssg  46975  negcncfg  46985  cncficcgt0  46992  fprodcncf  47004  fprodsubrecnncnvlem  47011  fprodaddrecnncnvlem  47013  dvsinax  47017  dvasinbx  47024  dvdivf  47026  ioodvbdlimc1lem2  47036  ioodvbdlimc2lem  47038  dvnmptdivc  47042  dvxpaek  47044  dvnxpaek  47046  dvnmul  47047  dvnprodlem2  47051  ibliccsinexp  47055  itgsinexplem1  47058  itgsinexp  47059  iblempty  47069  itgcoscmulx  47073  itgsincmulx  47078  itgioocnicc  47081  iblcncfioo  47082  itgsbtaddcnst  47086  volioofmpt  47098  volicofmpt  47101  stoweidlem4  47108  stirlinglem5  47182  dirkerval  47195  dirkertrigeq  47205  dirkeritg  47206  dirkercncflem2  47208  dirkercncflem4  47210  fourierdlem16  47227  fourierdlem18  47229  fourierdlem21  47232  fourierdlem22  47233  fourierdlem28  47239  fourierdlem39  47250  fourierdlem40  47251  fourierdlem41  47252  fourierdlem53  47263  fourierdlem56  47266  fourierdlem57  47267  fourierdlem60  47270  fourierdlem61  47271  fourierdlem68  47278  fourierdlem73  47283  fourierdlem74  47284  fourierdlem75  47285  fourierdlem76  47286  fourierdlem78  47288  fourierdlem81  47291  fourierdlem82  47292  fourierdlem83  47293  fourierdlem84  47294  fourierdlem85  47295  fourierdlem88  47298  fourierdlem90  47300  fourierdlem92  47302  fourierdlem93  47303  fourierdlem95  47305  fourierdlem97  47307  fourierdlem101  47311  fourierdlem103  47313  fourierdlem104  47314  fourierdlem111  47321  fourierdlem112  47322  sqwvfoura  47332  sqwvfourb  47333  fouriersw  47335  elaa2lem  47337  etransclem4  47342  etransclem17  47355  etransclem18  47356  etransclem32  47370  etransclem46  47384  sge0z  47479  sge0revalmpt  47482  sge0tsms  47484  sge0sup  47495  sge0iunmptlemre  47519  sge0iun  47523  sge0xaddlem2  47538  ismeannd  47571  psmeasurelem  47574  meaiuninclem  47584  meaiininclem  47590  caratheodory  47632  isomenndlem  47634  ovnval  47645  hoicvrrex  47660  ovnlecvr  47662  ovncvrrp  47668  ovn0lem  47669  ovnsubaddlem1  47674  hoidmv1lelem2  47696  hoidmv1le  47698  hoidmvlelem3  47701  ovnhoilem2  47706  ovnhoi  47707  ovnlecvr2  47714  ovncvr2  47715  hspmbllem2  47731  ovolval2lem  47747  ovolval3  47751  ovolval5lem1  47756  ovolval5lem2  47757  ovnovollem1  47760  ovnovollem2  47761  vonioolem1  47784  vonicclem1  47787  vonct  47797  smflim  47881  smfinflem  47921  smflimsuplem5  47928  smfliminflem  47934  cfsetsnfsetfv  48221  fundcmpsurbijinjpreimafv  48583  fundcmpsurinjimaid  48587  fdmdifeqresdif  49548  ply1mulgsumlem2  49593  lincvalsc0  49627  linc0scn0  49629  lincdifsn  49630  lincsum  49635  lincscm  49636  lindslinindimp2lem4  49667  lindslinindsimp2lem5  49668  lincresunit3lem2  49686  1arymaptfo  49849  itcovalpclem1  49876  itcovalpclem2  49877  itcovalt2lem1  49881  itcovalt2lem2  49882  tposcurf1  50515  tposcurf2  50516  diag1  50520  fuco22  50555  fucocolem2  50570  fucocolem3  50571  fucocolem4  50572  fucoco  50573  fucolid  50577  fucorid  50578  postcofval  50590  precofval  50596  precofvalALT  50597  precofval2  50598  fucoppcco  50638  termcpostfix  50766  islmd  50942  iscmd  50943  aacllem  51108  veronesematrowd  51150  veronesematrowexpd  51151  veroquadmodzerod  51153  amgmwlem  51156