Theorem mpteq2dva 5206

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   = wceq 1570   ∈ wcel 2146   ↦ cmpt 5194

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-ext 2737

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-sb 2100  df-clab 2744  df-cleq 2757  df-clel 2840  df-opab 5176  df-mpt 5195

This theorem is used by:  mpteq2dv  5207  mpteq2ia  5208  2fvcoidd  7301  offval  7689  offval2  7700  coof  7704  caofinvl  7712  caofcom  7717  caofass  7720  caofdi  7722  caofdir  7723  caonncan  7724  curry1  8101  curry2  8104  mpocurryd  8267  pw2f1olem  9072  mapxpen  9134  xpmapenlem  9135  cantnfp1  9653  cantnflem1d  9660  cantnflem1  9661  cnfcom2lem  9673  dfac12lem1  10139  seqof  14108  seqof2  14109  swrdswrd  14759  repswswrd  14840  repswrevw  14843  revco  14890  ccatco  14891  repsco  14896  ofccat  15025  lo1eq  15638  rlimeq  15639  lo1mul2  15699  o1dif  15700  lo1sub  15701  rlimdiv  15716  caucvgr  15746  sumeq1  15759  fsumrlim  15881  fsumo1  15882  climfsum  15890  geomulcvg  15948  vdwlem8  17065  prmgapprmo  17139  restid2  17500  pwsplusgval  17561  pwsmulrval  17562  pwsvscafval  17565  qusin  17615  xpsaddlem  17644  xpsvsca  17648  catidd  17753  fuclid  18043  fucrid  18044  fucass  18045  setcepi  18162  prf1st  18277  prf2nd  18278  1st2ndprf  18279  curfcl  18305  curfuncf  18311  diag2  18318  curf2ndf  18320  hof2val  18329  hofcllem  18331  hofcl  18332  yonedalem4a  18348  yonedalem4c  18350  yonedalem3b  18352  yonedainv  18354  yonffthlem  18355  prdssgrpd  18812  prdsidlem  18850  prdsmndd  18851  mhmvlin  18882  pwsco2mhm  18915  frmdup3lem  18948  frmdup3  18949  smndex1gid  18986  smndex1gidOLD  18987  smndex1igidOLD  18989  grpinvpropd  19104  prdsinvlem  19138  pwsinvg  19142  pwssub  19143  galactghm  19497  cayleylem1  19505  pmtrprfval  19580  sylow1lem2  19692  sylow3lem1  19720  efginvrel1  19821  frgpup3lem  19870  frgpup3  19871  prdscmnd  19954  iscyggen  19973  gsumval3  20000  gsumcllem  20001  gsumzsplit  20020  gsumsub  20041  gsummptf1o  20056  gsum2d  20065  gsum2d2  20067  gsumxp  20069  prdsgsum  20074  telgsumfz  20083  telgsumfz0  20085  telgsum  20087  dprdfsub  20116  dprdfeq0  20117  dprddisj2  20134  dprd2d2  20139  dpjidcl  20153  ablfaclem2  20181  ablfac2  20184  prdsmgp  20250  prdsrngd  20277  srgbinomlem3  20333  srgbinomlem4  20334  srgbinomlem  20335  gsumdixp  20425  prdsringd  20427  pwsgprod  20436  prdslmodd  21119  mulgrhm2  21657  frgpcyg  21752  freshmansdream  21753  evpmodpmf1o  21775  phlpropd  21834  frlmphl  21960  uvcresum  21972  frlmup1  21977  asclpropd  22076  psrass1lem  22112  psrlinv  22134  psrass1  22142  psrdi  22143  psrdir  22144  psrass23l  22145  psrcom  22146  psrass23  22147  resspsrmul  22154  mplsubrglem  22182  mplmonmul  22216  mplcoe1  22217  mplcoe5  22220  mplcoe4  22251  evlslem3  22260  evlslem1  22262  evlsvvval  22273  rhmcomulmpl  22304  evlsevl  22312  selvvvval  22322  mhpmulcl  22341  psdmplcl  22354  psdadd  22355  psdmul  22358  psdmvr  22361  psrplusgpropd  22424  psropprmul  22426  coe1mul2  22459  coe1tm  22463  coe1tmmul2  22466  coe1tmmul  22467  coe1pwmul  22469  cply1mul  22485  ply1coe  22487  eqcoe1ply1eq  22488  lply1binomsc  22500  evl1gsummon  22554  evls1fpws  22558  mamures  22583  grpvrinv  22585  mamuass  22588  mamudi  22589  mamudir  22590  mamuvs1  22591  mamuvs2  22592  mpomatmul  22632  mamutpos  22644  madetsumid  22647  dmatmul  22683  scmatscm  22699  1mavmul  22734  mavmulass  22735  mvmumamul1  22740  mulmarep1gsum1  22759  mulmarep1gsum2  22760  mdetleib2  22774  mdetfval1  22776  mdet0pr  22778  mdetdiag  22785  mdetdiagid  22786  mdetrlin  22788  mdetrsca  22789  mdetralt  22794  mdetunilem9  22806  gsummatr01  22845  smadiadetlem1a  22849  smadiadetlem3  22854  smadiadetlem4  22855  cpmatmcllem  22904  mat2pmatmul  22917  decpmatmullem  22957  decpmatmul  22958  pmatcollpw1lem2  22961  pmatcollpw  22967  pmatcollpw3lem  22969  pmatcollpwscmat  22977  idpm2idmp  22987  mp2pm2mplem3  22994  mp2pm2mplem4  22995  mp2pm2mplem5  22996  mp2pm2mp  22997  pm2mpghm  23002  pm2mpmhmlem2  23005  monmat2matmon  23010  pm2mp  23011  chpdmat  23027  chpscmat  23028  chpscmatgsumbin  23030  chpscmatgsummon  23031  chp0mat  23032  chpidmat  23033  chfacfscmulgsum  23046  chfacfpmmulgsum  23050  chfacfpmmulgsum2  23051  cayhamlem1  23052  cpmidgsumm2pm  23055  cpmidpmat  23059  cpmadugsumlemB  23060  cpmadugsumlemC  23061  cpmadugsumlemF  23062  cpmadumatpoly  23069  cayhamlem3  23073  cayhamlem4  23074  cayleyhamilton0  23075  cayleyhamiltonALT  23077  neiptopnei  23318  neiptopreu  23319  ptcnplem  23807  cnmpt1t  23851  cnmpt12  23853  cnmptkp  23866  cnmptk1  23867  cnmpt1k  23868  cnmptkk  23869  cnmptk1p  23871  cnmpt2k  23874  qtopeu  23902  pt1hmeo  23992  ptunhmeo  23994  xkocnv  24000  xkohmeo  24001  flfcnp2  24193  cnmpt1plusg  24273  istgp2  24277  tmdmulg  24278  tgpmulg  24279  tmdgsum  24281  subgtgp  24291  symgtgp  24292  tgpconncomp  24299  prdstgpd  24311  tsmsmhm  24332  tsmsadd  24333  tsmssub  24335  tgptsmscls  24336  tsmssplit  24338  tsmsxplem1  24339  tsmsxplem2  24340  cnmpt1vsca  24380  tlmtgp  24382  ustuqtoplem  24425  utopsnneip  24434  ressprdsds  24557  metuval  24735  nmfval0  24776  tngnm  24837  nmoeq0  24922  idnghm  24929  cnmpt1ds  25029  fsumcn  25058  expcn  25060  divccn  25061  divccncf  25094  negcncf  25110  copco  25206  pcopt  25210  pcopt2  25211  pcoass  25212  pi1xfrcnvlem  25244  cnmpt1ip  25435  rrxnm  25579  rrxds  25581  minveclem3b  25616  divcncf  25635  ovolctb  25678  ovoliunnul  25695  voliunlem3  25740  ovolfs2  25759  uniioombllem2  25771  vitalilem4  25799  vitalilem5  25800  ismbf  25816  mbfss  25834  mbfmulc2re  25836  mbfneg  25838  mbfpos  25839  mbfposb  25841  mbfadd  25849  mbfsub  25850  mbfmulc2  25851  mbfinf  25853  mbflimsup  25854  mbflimlem  25855  i1fpos  25894  i1fposd  25895  itg1climres  25902  mbfmul  25914  itg2mulc  25935  itg2i1fseq  25943  itg2cnlem1  25949  itg2cnlem2  25950  itgresr  25967  iblneg  25991  i1fibl  25996  itgitg1  25997  iblsub  26010  itgfsum  26015  itgmulc2lem1  26020  limcmpt  26071  limccnp  26079  limcco  26081  dvreslem  26097  dvres2lem  26098  dvidlem  26103  dvcnp2  26108  dvaddbr  26126  dvmulbr  26127  dvmulf  26131  dvcmulf  26133  dvcobr  26134  dvcof  26136  dvcjbr  26137  dvcj  26138  dvfre  26139  dvexp  26141  dvexp2  26142  dvrec  26143  dvmptcmul  26152  dvmptdivc  26153  dvmptneg  26154  dvmptsub  26155  dvmptre  26157  dvmptim  26158  dvrecg  26161  dvmptdiv  26162  dvmptfsum  26163  dvcnvlem  26164  dvcnv  26165  dvexp3  26166  dvef  26168  dvsincos  26169  dv11cn  26189  lhop2  26203  lhop  26204  ftc2  26232  itgparts  26235  itgsubstlem  26236  mdegfval  26248  mdegmullem  26264  ply1termlem  26389  plypow  26391  plyconst  26392  plyeq0lem  26396  plypf1  26398  plyaddlem1  26399  plymullem1  26400  coeeulem  26410  coeidlem  26423  plyco  26427  coeeq2  26428  0dgr  26431  0dgrb  26432  dgrcolem1  26459  dgrcolem2  26460  plycjlem  26462  plymul02  26470  plyn0mulidp  26471  plymulidp  26472  dvply1  26474  dvply2g  26475  plydiveu  26488  plyremlem  26494  elqaalem3  26511  taylfval  26551  dvtaylp  26562  taylthlem1  26565  taylthlem2  26566  ulmshft  26582  mtestbdd  26597  iblulm  26599  itgulm2  26601  pserulm  26614  psercn2  26615  pserdvlem2  26620  pserdv  26621  pserdv2  26622  abelthlem1  26623  abelthlem3  26625  advlog  26848  advlogexp  26849  dvcxp1  26934  dvcxp2  26935  dvcncxp1  26937  sqrtcn  26944  loglesqrt  26955  dvatan  27129  atantayl2  27132  atantayl3  27133  leibpi  27136  rlimcnp2  27160  efrlim  27163  dfef2  27164  cxp2lim  27170  divsqrtsumlem  27173  lgamgulmlem2  27223  lgamgulm2  27229  lgamcvglem  27233  gamcvg2lem  27252  ftalem7  27272  basellem9  27282  muinv  27386  logfacrlim  27417  logexprlim  27418  dchrmullid  27445  dchrinvcl  27446  lgseisenlem3  27570  lgseisenlem4  27571  chtppilimlem2  27667  chebbnd2  27670  chpchtlim  27672  chpo1ub  27673  rpvmasumlem  27680  dchrmusumlema  27686  dchrvmasumlem1  27688  dchrvmasumiflem2  27695  dchrisum0fno1  27704  rpvmasum2  27705  dchrisum0lema  27707  dchrisum0lem1  27709  dchrisum0lem2a  27710  dchrisum0lem2  27711  dchrisum0  27713  dchrmusumlem  27715  dchrvmasumlem  27716  rpvmasum  27719  rplogsum  27720  logdivsum  27726  mulog2sumlem3  27729  vmalogdivsum2  27731  vmalogdivsum  27732  2vmadivsumlem  27733  logsqvma2  27736  log2sumbnd  27737  selberglem2  27739  selberg3lem1  27750  selberg3  27752  selberg4lem1  27753  selberg4  27754  pntrsumo1  27758  selberg3r  27762  selberg4r  27763  selberg34r  27764  pntrlog2bndlem2  27771  pntrlog2bndlem4  27773  pntrlog2bndlem5  27774  pntrlog2bndlem6  27776  padicabvf  27824  padicabvcxp  27825  mirval  28961  crctcshlem4  30198  clwlknf1oclwwlkn  30464  eucrct2eupth  30625  chscllem4  32021  brafnmul  32332  kbmul  32336  cofmpt2  33008  ofresid  33016  ofoprabco  33038  fmptunsnop  33074  fcobijfs  33095  fcobijfs2  33096  gsummpt2d  33392  gsummptres  33395  gsummptres2  33396  gsummptf1od  33398  gsummptp1  33400  gsummptfsf1o  33403  gsumfs2d  33404  gsumpart  33406  gsumhashmul  33410  gsummulsubdishift1  33411  gsummulsubdishift2  33412  gsumwrd2dccat  33421  fzto1st1  33445  fzto1st  33446  elrgspnlem1  33585  elrgspnlem2  33586  elrgspnlem3  33587  elrgspnlem4  33588  elrgspnsubrunlem1  33590  elrgspnsubrunlem2  33591  qusbas2  33738  qusima  33740  elrspunidl  33759  elrspunsn  33760  rprmdvdsprod  33847  ressply1evls1  33878  evl1deg1  33889  evl1deg2  33890  evl1deg3  33891  gsummoncoe1fzo  33910  mplasclco  33929  selvply1rhmlemb  33932  selvply1rhmlem2  33934  selvply1rhmlem4  33936  selvply1rhm0  33939  mplmulmvr  33952  evlextv  33955  mplvrpmga  33958  mplvrpmmhm  33959  mplvrpmrhm  33960  psrgsum  33961  psrmonmul  33963  issply  33974  esplyfval0  33977  esplyfval3  33985  esplyfval1  33986  esplyfvaln  33987  esplyind  33988  vietalem  33992  lbsdiflsp0  34039  fedgmullem1  34042  fedgmullem2  34043  fldextrspunlsplem  34086  fldextrspunlsp  34087  extdgfialglem2  34106  mdetpmtr1  34236  mdetlap  34245  xrge0mulc1cn  34354  esumval  34459  esumsnf  34477  esumpcvgval  34491  esumcvg  34499  esumcvgsum  34501  esumsup  34502  ofcfeqd2  34514  meascnbl  34633  sitgval  34746  probmeasb  34844  cndprobprob  34852  dstfrvclim1  34892  ballotlemfval  34904  ballotlemsval  34923  ballotlemieq  34931  signsplypnf  34961  signstfv  34974  signstfvn  34980  signstfvp  34982  itgexpif  35017  logdivsqrle  35061  ptpconn  35738  cvmliftlem6  35795  cvmliftphtlem  35822  cvmlift3lem5  35828  elmrsubrn  36025  msubfval  36029  msubco  36036  divcnvlin  36238  knoppcnlem9  37123  knoppcnlem10  37124  knoppcnlem11  37125  bj-finsumval0  37962  curf  38282  matunitlindflem1  38300  matunitlindflem2  38301  poimirlem3  38307  poimirlem15  38319  poimirlem16  38320  poimirlem17  38321  poimirlem19  38323  poimirlem20  38324  broucube  38338  ovoliunnfl  38346  voliunnfl  38348  volsupnfl  38349  mbfposadd  38351  itg2addnclem  38355  itg2addnclem3  38357  itg2addnc  38358  itgaddnclem2  38363  itgaddnc  38364  iblsubnc  38365  itgsubnc  38366  itgmulc2nclem1  38370  itgmulc2nclem2  38371  itgmulc2nc  38372  itgabsnc  38373  ftc1cnnclem  38375  ftc1anclem3  38379  ftc1anclem5  38381  ftc1anclem6  38382  ftc1anclem8  38384  ftc1anc  38385  ftc2nc  38386  areacirclem1  38392  areacirclem2  38393  areacirclem4  38395  areacirc  38397  upixp  38413  lcmineqlem8  42836  lcmineqlem12  42840  dvrelog2b  42866  dvrelogpow2b  42868  aks4d1p1p6  42873  aks4d1p1p5  42875  aks6d1c1  42916  aks6d1c5lem3  42937  sticksstones12a  42957  sticksstones12  42958  sticksstones19  42965  aks6d1c6lem1  42970  aks6d1c6lem4  42973  aks6d1c7lem3  42982  qsalrel  43042  rhmcomulpsr  43347  evlselv  43354  fsuppssindlem1  43356  fsuppssind  43358  mhphf  43362  mzpsubst  43512  mzprename  43513  mzpcompact2lem  43515  eldioph2  43526  rabdiophlem2  43562  mendlmod  43949  mendassa  43950  areaquad  43976  fsovcnvlem  44772  hashnzfzclim  45065  expgrowthi  45076  expgrowth  45078  uzmptshftfval  45089  dvradcnv2  45090  binomcxplemrat  45093  binomcxplemfrat  45094  binomcxplemradcnv  45095  binomcxplemdvbinom  45096  binomcxplemcvg  45097  binomcxplemdvsum  45098  binomcxplemnotnn0  45099  mulc1cncfg  46338  expcnfg  46340  fprodcnlem  46348  clim1fr1  46350  divcnvg  46376  sublimc  46399  reclimc  46400  divlimc  46403  limsupresico  46447  limsuppnfdlem  46448  limsupvaluz  46455  supcnvlimsupmpt  46488  liminfresico  46518  climliminflimsupd  46548  cncfmptssg  46618  negcncfg  46628  cncficcgt0  46635  fprodcncf  46647  fprodsubrecnncnvlem  46654  fprodaddrecnncnvlem  46656  dvsinax  46660  dvasinbx  46667  dvdivf  46669  ioodvbdlimc1lem2  46679  ioodvbdlimc2lem  46681  dvnmptdivc  46685  dvxpaek  46687  dvnxpaek  46689  dvnmul  46690  dvnprodlem2  46694  ibliccsinexp  46698  itgsinexplem1  46701  itgsinexp  46702  iblempty  46712  itgcoscmulx  46716  itgsincmulx  46721  itgioocnicc  46724  iblcncfioo  46725  itgsbtaddcnst  46729  volioofmpt  46741  volicofmpt  46744  stoweidlem4  46751  stirlinglem5  46825  dirkerval  46838  dirkertrigeq  46848  dirkeritg  46849  dirkercncflem2  46851  dirkercncflem4  46853  fourierdlem16  46870  fourierdlem18  46872  fourierdlem21  46875  fourierdlem22  46876  fourierdlem28  46882  fourierdlem39  46893  fourierdlem40  46894  fourierdlem41  46895  fourierdlem53  46906  fourierdlem56  46909  fourierdlem57  46910  fourierdlem60  46913  fourierdlem61  46914  fourierdlem68  46921  fourierdlem73  46926  fourierdlem74  46927  fourierdlem75  46928  fourierdlem76  46929  fourierdlem78  46931  fourierdlem81  46934  fourierdlem82  46935  fourierdlem83  46936  fourierdlem84  46937  fourierdlem85  46938  fourierdlem88  46941  fourierdlem90  46943  fourierdlem92  46945  fourierdlem93  46946  fourierdlem95  46948  fourierdlem97  46950  fourierdlem101  46954  fourierdlem103  46956  fourierdlem104  46957  fourierdlem111  46964  fourierdlem112  46965  sqwvfoura  46975  sqwvfourb  46976  fouriersw  46978  elaa2lem  46980  etransclem4  46985  etransclem17  46998  etransclem18  46999  etransclem32  47013  etransclem46  47027  sge0z  47122  sge0revalmpt  47125  sge0tsms  47127  sge0sup  47138  sge0iunmptlemre  47162  sge0iun  47166  sge0xaddlem2  47181  ismeannd  47214  psmeasurelem  47217  meaiuninclem  47227  meaiininclem  47233  caratheodory  47275  isomenndlem  47277  ovnval  47288  hoicvrrex  47303  ovnlecvr  47305  ovncvrrp  47311  ovn0lem  47312  ovnsubaddlem1  47317  hoidmv1lelem2  47339  hoidmv1le  47341  hoidmvlelem3  47344  ovnhoilem2  47349  ovnhoi  47350  ovnlecvr2  47357  ovncvr2  47358  hspmbllem2  47374  ovolval2lem  47390  ovolval3  47394  ovolval5lem1  47399  ovolval5lem2  47400  ovnovollem1  47403  ovnovollem2  47404  vonioolem1  47427  vonicclem1  47430  vonct  47440  smflim  47524  smfinflem  47564  smflimsuplem5  47571  smfliminflem  47577  cfsetsnfsetfv  47827  fundcmpsurbijinjpreimafv  48189  fundcmpsurinjimaid  48193  fdmdifeqresdif  49155  ply1mulgsumlem2  49200  lincvalsc0  49234  linc0scn0  49236  lincdifsn  49237  lincsum  49242  lincscm  49243  lindslinindimp2lem4  49274  lindslinindsimp2lem5  49275  lincresunit3lem2  49293  1arymaptfo  49456  itcovalpclem1  49483  itcovalpclem2  49484  itcovalt2lem1  49488  itcovalt2lem2  49489  tposcurf1  50110  tposcurf2  50111  diag1  50115  fuco22  50150  fucocolem2  50165  fucocolem3  50166  fucocolem4  50167  fucoco  50168  fucolid  50172  fucorid  50173  postcofval  50175  precofval  50178  precofvalALT  50179  precofval2  50180  fucoppcco  50220  islmd  50476  iscmd  50477  aacllem  50654  amgmwlem  50683