Theorem mpteq2dva 5178

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

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1542   ∈ wcel 2114   ↦ cmpt 5166

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-sb 2069  df-clab 2715  df-cleq 2728  df-clel 2811  df-opab 5148  df-mpt 5167

This theorem is referenced by:  mpteq2dv  5179  mpteq2ia  5180  2fvcoidd  7252  offval  7640  offval2  7651  coof  7655  caofinvl  7663  caofcom  7668  caofass  7671  caofdi  7673  caofdir  7674  caonncan  7675  curry1  8054  curry2  8057  mpocurryd  8219  pw2f1olem  9019  mapxpen  9081  xpmapenlem  9082  cantnfp1  9602  cantnflem1d  9609  cantnflem1  9610  cnfcom2lem  9622  dfac12lem1  10066  seqof  14021  seqof2  14022  swrdswrd  14667  repswswrd  14746  repswrevw  14749  revco  14796  ccatco  14797  repsco  14802  ofccat  14931  lo1eq  15530  rlimeq  15531  lo1mul2  15591  o1dif  15592  lo1sub  15593  rlimdiv  15608  caucvgr  15638  sumeq1  15651  fsumrlim  15774  fsumo1  15775  climfsum  15783  geomulcvg  15841  vdwlem8  16959  prmgapprmo  17033  restid2  17393  pwsplusgval  17454  pwsmulrval  17455  pwsvscafval  17458  qusin  17508  xpsaddlem  17537  xpsvsca  17541  catidd  17646  fuclid  17936  fucrid  17937  fucass  17938  setcepi  18055  prf1st  18170  prf2nd  18171  1st2ndprf  18172  curfcl  18198  curfuncf  18204  diag2  18211  curf2ndf  18213  hof2val  18222  hofcllem  18224  hofcl  18225  yonedalem4a  18241  yonedalem4c  18243  yonedalem3b  18245  yonedainv  18247  yonffthlem  18248  prdssgrpd  18701  prdsidlem  18737  prdsmndd  18738  mhmvlin  18769  pwsco2mhm  18801  frmdup3lem  18834  frmdup3  18835  smndex1gid  18872  smndex1gidOLD  18873  smndex1igidOLD  18875  grpinvpropd  18991  prdsinvlem  19025  pwsinvg  19029  pwssub  19030  galactghm  19379  cayleylem1  19387  pmtrprfval  19462  sylow1lem2  19574  sylow3lem1  19602  efginvrel1  19703  frgpup3lem  19752  frgpup3  19753  prdscmnd  19836  iscyggen  19855  gsumval3  19882  gsumcllem  19883  gsumzsplit  19902  gsumsub  19923  gsummptf1o  19938  gsum2d  19947  gsum2d2  19949  gsumxp  19951  prdsgsum  19956  telgsumfz  19965  telgsumfz0  19967  telgsum  19969  dprdfsub  19998  dprdfeq0  19999  dprddisj2  20016  dprd2d2  20021  dpjidcl  20035  ablfaclem2  20063  ablfac2  20066  prdsmgp  20132  prdsrngd  20157  srgbinomlem3  20209  srgbinomlem4  20210  srgbinomlem  20211  gsumdixp  20298  prdsringd  20300  pwsgprod  20309  prdslmodd  20964  mulgrhm2  21458  frgpcyg  21553  freshmansdream  21554  evpmodpmf1o  21576  phlpropd  21635  frlmphl  21761  uvcresum  21773  frlmup1  21778  asclpropd  21877  psrass1lem  21912  psrlinv  21934  psrass1  21942  psrdi  21943  psrdir  21944  psrass23l  21945  psrcom  21946  psrass23  21947  resspsrmul  21954  mplsubrglem  21982  mplmonmul  22014  mplcoe1  22015  mplcoe5  22018  mplcoe4  22049  evlslem3  22058  evlslem1  22060  evlsvvval  22071  mhpmulcl  22115  psdmplcl  22128  psdadd  22129  psdmul  22132  psdmvr  22135  psrplusgpropd  22199  psropprmul  22201  coe1mul2  22234  coe1tm  22238  coe1tmmul2  22241  coe1tmmul  22242  coe1pwmul  22244  cply1mul  22261  ply1coe  22263  eqcoe1ply1eq  22264  lply1binomsc  22276  evl1gsummon  22330  evls1fpws  22334  rhmcomulmpl  22347  mamures  22362  grpvrinv  22364  mamuass  22367  mamudi  22368  mamudir  22369  mamuvs1  22370  mamuvs2  22371  mpomatmul  22411  mamutpos  22423  madetsumid  22426  dmatmul  22462  scmatscm  22478  1mavmul  22513  mavmulass  22514  mvmumamul1  22519  mulmarep1gsum1  22538  mulmarep1gsum2  22539  mdetleib2  22553  mdetfval1  22555  mdet0pr  22557  mdetdiag  22564  mdetdiagid  22565  mdetrlin  22567  mdetrsca  22568  mdetralt  22573  mdetunilem9  22585  gsummatr01  22624  smadiadetlem1a  22628  smadiadetlem3  22633  smadiadetlem4  22634  cpmatmcllem  22683  mat2pmatmul  22696  decpmatmullem  22736  decpmatmul  22737  pmatcollpw1lem2  22740  pmatcollpw  22746  pmatcollpw3lem  22748  pmatcollpwscmat  22756  idpm2idmp  22766  mp2pm2mplem3  22773  mp2pm2mplem4  22774  mp2pm2mplem5  22775  mp2pm2mp  22776  pm2mpghm  22781  pm2mpmhmlem2  22784  monmat2matmon  22789  pm2mp  22790  chpdmat  22806  chpscmat  22807  chpscmatgsumbin  22809  chpscmatgsummon  22810  chp0mat  22811  chpidmat  22812  chfacfscmulgsum  22825  chfacfpmmulgsum  22829  chfacfpmmulgsum2  22830  cayhamlem1  22831  cpmidgsumm2pm  22834  cpmidpmat  22838  cpmadugsumlemB  22839  cpmadugsumlemC  22840  cpmadugsumlemF  22841  cpmadumatpoly  22848  cayhamlem3  22852  cayhamlem4  22853  cayleyhamilton0  22854  cayleyhamiltonALT  22856  neiptopnei  23097  neiptopreu  23098  ptcnplem  23586  cnmpt1t  23630  cnmpt12  23632  cnmptkp  23645  cnmptk1  23646  cnmpt1k  23647  cnmptkk  23648  cnmptk1p  23650  cnmpt2k  23653  qtopeu  23681  pt1hmeo  23771  ptunhmeo  23773  xkocnv  23779  xkohmeo  23780  flfcnp2  23972  cnmpt1plusg  24052  istgp2  24056  tmdmulg  24057  tgpmulg  24058  tmdgsum  24060  subgtgp  24070  symgtgp  24071  tgpconncomp  24078  prdstgpd  24090  tsmsmhm  24111  tsmsadd  24112  tsmssub  24114  tgptsmscls  24115  tsmssplit  24117  tsmsxplem1  24118  tsmsxplem2  24119  cnmpt1vsca  24159  tlmtgp  24161  ustuqtoplem  24204  utopsnneip  24213  ressprdsds  24336  metuval  24514  nmfval0  24555  tngnm  24616  nmoeq0  24701  idnghm  24708  cnmpt1ds  24808  fsumcn  24837  expcn  24839  divccn  24840  divccncf  24873  negcncf  24889  copco  24985  pcopt  24989  pcopt2  24990  pcoass  24991  pi1xfrcnvlem  25023  cnmpt1ip  25214  rrxnm  25358  rrxds  25360  minveclem3b  25395  divcncf  25414  ovolctb  25457  ovoliunnul  25474  voliunlem3  25519  ovolfs2  25538  uniioombllem2  25550  vitalilem4  25578  vitalilem5  25579  ismbf  25595  mbfss  25613  mbfmulc2re  25615  mbfneg  25617  mbfpos  25618  mbfposb  25620  mbfadd  25628  mbfsub  25629  mbfmulc2  25630  mbfinf  25632  mbflimsup  25633  mbflimlem  25634  i1fpos  25673  i1fposd  25674  itg1climres  25681  mbfmul  25693  itg2mulc  25714  itg2i1fseq  25722  itg2cnlem1  25728  itg2cnlem2  25729  itgresr  25746  iblneg  25770  i1fibl  25775  itgitg1  25776  iblsub  25789  itgfsum  25794  itgmulc2lem1  25799  limcmpt  25850  limccnp  25858  limcco  25860  dvreslem  25876  dvres2lem  25877  dvidlem  25882  dvcnp2  25887  dvaddbr  25905  dvmulbr  25906  dvmulf  25910  dvcmulf  25912  dvcobr  25913  dvcof  25915  dvcjbr  25916  dvcj  25917  dvfre  25918  dvexp  25920  dvexp2  25921  dvrec  25922  dvmptcmul  25931  dvmptdivc  25932  dvmptneg  25933  dvmptsub  25934  dvmptre  25936  dvmptim  25937  dvrecg  25940  dvmptdiv  25941  dvmptfsum  25942  dvcnvlem  25943  dvcnv  25944  dvexp3  25945  dvef  25947  dvsincos  25948  dv11cn  25968  lhop2  25982  lhop  25983  ftc2  26011  itgparts  26014  itgsubstlem  26015  mdegfval  26027  mdegmullem  26043  ply1termlem  26168  plypow  26170  plyconst  26171  plyeq0lem  26175  plypf1  26177  plyaddlem1  26178  plymullem1  26179  coeeulem  26189  coeidlem  26202  plyco  26206  coeeq2  26207  0dgr  26210  0dgrb  26211  dgrcolem1  26238  dgrcolem2  26239  plycjlem  26241  dvply1  26250  dvply2g  26251  plydiveu  26264  plyremlem  26270  elqaalem3  26287  taylfval  26324  dvtaylp  26335  taylthlem1  26338  taylthlem2  26339  ulmshft  26355  mtestbdd  26370  iblulm  26372  itgulm2  26374  pserulm  26387  psercn2  26388  pserdvlem2  26393  pserdv  26394  pserdv2  26395  abelthlem1  26396  abelthlem3  26398  advlog  26618  advlogexp  26619  dvcxp1  26704  dvcxp2  26705  dvcncxp1  26707  sqrtcn  26714  loglesqrt  26725  dvatan  26899  atantayl2  26902  atantayl3  26903  leibpi  26906  rlimcnp2  26930  efrlim  26933  dfef2  26934  cxp2lim  26940  divsqrtsumlem  26943  lgamgulmlem2  26993  lgamgulm2  26999  lgamcvglem  27003  gamcvg2lem  27022  ftalem7  27042  basellem9  27052  muinv  27156  logfacrlim  27187  logexprlim  27188  dchrmullid  27215  dchrinvcl  27216  lgseisenlem3  27340  lgseisenlem4  27341  chtppilimlem2  27437  chebbnd2  27440  chpchtlim  27442  chpo1ub  27443  rpvmasumlem  27450  dchrmusumlema  27456  dchrvmasumlem1  27458  dchrvmasumiflem2  27465  dchrisum0fno1  27474  rpvmasum2  27475  dchrisum0lema  27477  dchrisum0lem1  27479  dchrisum0lem2a  27480  dchrisum0lem2  27481  dchrisum0  27483  dchrmusumlem  27485  dchrvmasumlem  27486  rpvmasum  27489  rplogsum  27490  logdivsum  27496  mulog2sumlem3  27499  vmalogdivsum2  27501  vmalogdivsum  27502  2vmadivsumlem  27503  logsqvma2  27506  log2sumbnd  27507  selberglem2  27509  selberg3lem1  27520  selberg3  27522  selberg4lem1  27523  selberg4  27524  pntrsumo1  27528  selberg3r  27532  selberg4r  27533  selberg34r  27534  pntrlog2bndlem2  27541  pntrlog2bndlem4  27543  pntrlog2bndlem5  27544  pntrlog2bndlem6  27546  padicabvf  27594  padicabvcxp  27595  mirval  28723  crctcshlem4  29888  clwlknf1oclwwlkn  30154  eucrct2eupth  30315  chscllem4  31711  brafnmul  32022  kbmul  32026  cofmpt2  32707  ofresid  32715  ofoprabco  32737  fmptunsnop  32773  fcobijfs  32794  fcobijfs2  32795  gsummpt2d  33110  gsummptres  33113  gsummptres2  33114  gsummptf1od  33116  gsummptp1  33118  gsummptfsf1o  33121  gsumfs2d  33122  gsumpart  33124  gsumhashmul  33128  gsummulsubdishift1  33129  gsummulsubdishift2  33130  gsumwrd2dccat  33139  fzto1st1  33163  fzto1st  33164  elrgspnlem1  33303  elrgspnlem2  33304  elrgspnlem3  33305  elrgspnlem4  33306  elrgspnsubrunlem1  33308  elrgspnsubrunlem2  33309  qusbas2  33466  qusima  33468  elrspunidl  33488  elrspunsn  33489  rprmdvdsprod  33594  ressply1evls1  33625  evl1deg1  33636  evl1deg2  33637  evl1deg3  33638  gsummoncoe1fzo  33657  mplmulmvr  33683  evlextv  33686  mplvrpmga  33689  mplvrpmmhm  33690  mplvrpmrhm  33691  psrgsum  33692  psrmonmul  33694  issply  33705  esplyfval0  33708  esplyfval3  33716  esplyfval1  33717  esplyfvaln  33718  esplyind  33719  vietalem  33723  lbsdiflsp0  33770  fedgmullem1  33773  fedgmullem2  33774  fldextrspunlsplem  33817  fldextrspunlsp  33818  extdgfialglem2  33837  mdetpmtr1  33967  mdetlap  33976  xrge0mulc1cn  34085  esumval  34190  esumsnf  34208  esumpcvgval  34222  esumcvg  34230  esumcvgsum  34232  esumsup  34233  ofcfeqd2  34245  meascnbl  34363  sitgval  34476  probmeasb  34574  cndprobprob  34582  dstfrvclim1  34622  ballotlemfval  34634  ballotlemsval  34653  ballotlemieq  34661  plymul02  34690  plymulx0  34691  plymulx  34692  signsplypnf  34694  signstfv  34707  signstfvn  34713  signstfvp  34715  itgexpif  34750  logdivsqrle  34794  ptpconn  35415  cvmliftlem6  35472  cvmliftphtlem  35499  cvmlift3lem5  35505  elmrsubrn  35702  msubfval  35706  msubco  35713  divcnvlin  35915  knoppcnlem9  36761  knoppcnlem10  36762  knoppcnlem11  36763  bj-finsumval0  37599  curf  37919  matunitlindflem1  37937  matunitlindflem2  37938  poimirlem3  37944  poimirlem15  37956  poimirlem16  37957  poimirlem17  37958  poimirlem19  37960  poimirlem20  37961  broucube  37975  ovoliunnfl  37983  voliunnfl  37985  volsupnfl  37986  mbfposadd  37988  itg2addnclem  37992  itg2addnclem3  37994  itg2addnc  37995  itgaddnclem2  38000  itgaddnc  38001  iblsubnc  38002  itgsubnc  38003  itgmulc2nclem1  38007  itgmulc2nclem2  38008  itgmulc2nc  38009  itgabsnc  38010  ftc1cnnclem  38012  ftc1anclem3  38016  ftc1anclem5  38018  ftc1anclem6  38019  ftc1anclem8  38021  ftc1anc  38022  ftc2nc  38023  areacirclem1  38029  areacirclem2  38030  areacirclem4  38032  areacirc  38034  upixp  38050  lcmineqlem8  42475  lcmineqlem12  42479  dvrelog2b  42505  dvrelogpow2b  42507  aks4d1p1p6  42512  aks4d1p1p5  42514  aks6d1c1  42555  aks6d1c5lem3  42576  sticksstones12a  42596  sticksstones12  42597  sticksstones19  42604  aks6d1c6lem1  42609  aks6d1c6lem4  42612  aks6d1c7lem3  42621  qsalrel  42680  rhmcomulpsr  42994  evlsevl  43007  selvvvval  43018  evlselv  43020  fsuppssindlem1  43024  fsuppssind  43026  mhphf  43030  mzpsubst  43180  mzprename  43181  mzpcompact2lem  43183  eldioph2  43194  rabdiophlem2  43230  mendlmod  43617  mendassa  43618  areaquad  43644  fsovcnvlem  44440  hashnzfzclim  44749  expgrowthi  44760  expgrowth  44762  uzmptshftfval  44773  dvradcnv2  44774  binomcxplemrat  44777  binomcxplemfrat  44778  binomcxplemradcnv  44779  binomcxplemdvbinom  44780  binomcxplemcvg  44781  binomcxplemdvsum  44782  binomcxplemnotnn0  44783  mulc1cncfg  46019  expcnfg  46021  fprodcnlem  46029  clim1fr1  46031  divcnvg  46057  sublimc  46080  reclimc  46081  divlimc  46084  limsupresico  46128  limsuppnfdlem  46129  limsupvaluz  46136  supcnvlimsupmpt  46169  liminfresico  46199  climliminflimsupd  46229  cncfmptssg  46299  negcncfg  46309  cncficcgt0  46316  fprodcncf  46328  fprodsubrecnncnvlem  46335  fprodaddrecnncnvlem  46337  dvsinax  46341  dvasinbx  46348  dvdivf  46350  ioodvbdlimc1lem2  46360  ioodvbdlimc2lem  46362  dvnmptdivc  46366  dvxpaek  46368  dvnxpaek  46370  dvnmul  46371  dvnprodlem2  46375  ibliccsinexp  46379  itgsinexplem1  46382  itgsinexp  46383  iblempty  46393  itgcoscmulx  46397  itgsincmulx  46402  itgioocnicc  46405  iblcncfioo  46406  itgsbtaddcnst  46410  volioofmpt  46422  volicofmpt  46425  stoweidlem4  46432  stirlinglem5  46506  dirkerval  46519  dirkertrigeq  46529  dirkeritg  46530  dirkercncflem2  46532  dirkercncflem4  46534  fourierdlem16  46551  fourierdlem18  46553  fourierdlem21  46556  fourierdlem22  46557  fourierdlem28  46563  fourierdlem39  46574  fourierdlem40  46575  fourierdlem41  46576  fourierdlem53  46587  fourierdlem56  46590  fourierdlem57  46591  fourierdlem60  46594  fourierdlem61  46595  fourierdlem68  46602  fourierdlem73  46607  fourierdlem74  46608  fourierdlem75  46609  fourierdlem76  46610  fourierdlem78  46612  fourierdlem81  46615  fourierdlem82  46616  fourierdlem83  46617  fourierdlem84  46618  fourierdlem85  46619  fourierdlem88  46622  fourierdlem90  46624  fourierdlem92  46626  fourierdlem93  46627  fourierdlem95  46629  fourierdlem97  46631  fourierdlem101  46635  fourierdlem103  46637  fourierdlem104  46638  fourierdlem111  46645  fourierdlem112  46646  sqwvfoura  46656  sqwvfourb  46657  fouriersw  46659  elaa2lem  46661  etransclem4  46666  etransclem17  46679  etransclem18  46680  etransclem32  46694  etransclem46  46708  sge0z  46803  sge0revalmpt  46806  sge0tsms  46808  sge0sup  46819  sge0iunmptlemre  46843  sge0iun  46847  sge0xaddlem2  46862  ismeannd  46895  psmeasurelem  46898  meaiuninclem  46908  meaiininclem  46914  caratheodory  46956  isomenndlem  46958  ovnval  46969  hoicvrrex  46984  ovnlecvr  46986  ovncvrrp  46992  ovn0lem  46993  ovnsubaddlem1  46998  hoidmv1lelem2  47020  hoidmv1le  47022  hoidmvlelem3  47025  ovnhoilem2  47030  ovnhoi  47031  ovnlecvr2  47038  ovncvr2  47039  hspmbllem2  47055  ovolval2lem  47071  ovolval3  47075  ovolval5lem1  47080  ovolval5lem2  47081  ovnovollem1  47084  ovnovollem2  47085  vonioolem1  47108  vonicclem1  47111  vonct  47121  smflim  47205  smfinflem  47245  smflimsuplem5  47252  smfliminflem  47258  cfsetsnfsetfv  47505  fundcmpsurbijinjpreimafv  47867  fundcmpsurinjimaid  47871  fdmdifeqresdif  48818  ply1mulgsumlem2  48863  lincvalsc0  48897  linc0scn0  48899  lincdifsn  48900  lincsum  48905  lincscm  48906  lindslinindimp2lem4  48937  lindslinindsimp2lem5  48938  lincresunit3lem2  48956  1arymaptfo  49119  itcovalpclem1  49146  itcovalpclem2  49147  itcovalt2lem1  49151  itcovalt2lem2  49152  tposcurf1  49774  tposcurf2  49775  diag1  49779  fuco22  49814  fucocolem2  49829  fucocolem3  49830  fucocolem4  49831  fucoco  49832  fucolid  49836  fucorid  49837  postcofval  49839  precofval  49842  precofvalALT  49843  precofval2  49844  fucoppcco  49884  islmd  50140  iscmd  50141  aacllem  50276  amgmwlem  50277