Theorem mpteq2dva 5172

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

Syntax hints:   → wi 4   ∧ wa 396   = wceq 1547   ∈ wcel 2119   ↦ cmpt 5160

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2712

This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1787  df-sb 2074  df-clab 2719  df-cleq 2732  df-clel 2815  df-opab 5142  df-mpt 5161

This theorem is referenced by:  mpteq2dv  5173  mpteq2ia  5174  2fvcoidd  7248  offval  7636  offval2  7647  coof  7651  caofinvl  7659  caofcom  7664  caofass  7667  caofdi  7669  caofdir  7670  caonncan  7671  curry1  8050  curry2  8053  mpocurryd  8216  pw2f1olem  9016  mapxpen  9078  xpmapenlem  9079  cantnfp1  9600  cantnflem1d  9607  cantnflem1  9608  cnfcom2lem  9620  dfac12lem1  10064  seqof  14019  seqof2  14020  swrdswrd  14665  repswswrd  14744  repswrevw  14747  revco  14794  ccatco  14795  repsco  14800  ofccat  14929  lo1eq  15528  rlimeq  15529  lo1mul2  15589  o1dif  15590  lo1sub  15591  rlimdiv  15606  caucvgr  15636  sumeq1  15649  fsumrlim  15772  fsumo1  15773  climfsum  15781  geomulcvg  15839  vdwlem8  16957  prmgapprmo  17031  restid2  17391  pwsplusgval  17452  pwsmulrval  17453  pwsvscafval  17456  qusin  17506  xpsaddlem  17535  xpsvsca  17539  catidd  17644  fuclid  17934  fucrid  17935  fucass  17936  setcepi  18053  prf1st  18168  prf2nd  18169  1st2ndprf  18170  curfcl  18196  curfuncf  18202  diag2  18209  curf2ndf  18211  hof2val  18220  hofcllem  18222  hofcl  18223  yonedalem4a  18239  yonedalem4c  18241  yonedalem3b  18243  yonedainv  18245  yonffthlem  18246  prdssgrpd  18699  prdsidlem  18735  prdsmndd  18736  mhmvlin  18767  pwsco2mhm  18799  frmdup3lem  18832  frmdup3  18833  smndex1gid  18870  smndex1gidOLD  18871  smndex1igidOLD  18873  grpinvpropd  18989  prdsinvlem  19023  pwsinvg  19027  pwssub  19028  galactghm  19377  cayleylem1  19385  pmtrprfval  19460  sylow1lem2  19572  sylow3lem1  19600  efginvrel1  19701  frgpup3lem  19750  frgpup3  19751  prdscmnd  19834  iscyggen  19853  gsumval3  19880  gsumcllem  19881  gsumzsplit  19900  gsumsub  19921  gsummptf1o  19936  gsum2d  19945  gsum2d2  19947  gsumxp  19949  prdsgsum  19954  telgsumfz  19963  telgsumfz0  19965  telgsum  19967  dprdfsub  19996  dprdfeq0  19997  dprddisj2  20014  dprd2d2  20019  dpjidcl  20033  ablfaclem2  20061  ablfac2  20064  prdsmgp  20130  prdsrngd  20155  srgbinomlem3  20207  srgbinomlem4  20208  srgbinomlem  20209  gsumdixp  20296  prdsringd  20298  pwsgprod  20307  prdslmodd  20966  mulgrhm2  21460  frgpcyg  21555  freshmansdream  21556  evpmodpmf1o  21578  phlpropd  21637  frlmphl  21763  uvcresum  21775  frlmup1  21780  asclpropd  21879  psrass1lem  21915  psrlinv  21937  psrass1  21945  psrdi  21946  psrdir  21947  psrass23l  21948  psrcom  21949  psrass23  21950  resspsrmul  21957  mplsubrglem  21985  mplmonmul  22019  mplcoe1  22020  mplcoe5  22023  mplcoe4  22054  evlslem3  22063  evlslem1  22065  evlsvvval  22076  rhmcomulmpl  22107  evlsevl  22115  selvvvval  22125  mhpmulcl  22144  psdmplcl  22157  psdadd  22158  psdmul  22161  psdmvr  22164  psrplusgpropd  22227  psropprmul  22229  coe1mul2  22262  coe1tm  22266  coe1tmmul2  22269  coe1tmmul  22270  coe1pwmul  22272  cply1mul  22289  ply1coe  22291  eqcoe1ply1eq  22292  lply1binomsc  22304  evl1gsummon  22358  evls1fpws  22362  mamures  22387  grpvrinv  22389  mamuass  22392  mamudi  22393  mamudir  22394  mamuvs1  22395  mamuvs2  22396  mpomatmul  22436  mamutpos  22448  madetsumid  22451  dmatmul  22487  scmatscm  22503  1mavmul  22538  mavmulass  22539  mvmumamul1  22544  mulmarep1gsum1  22563  mulmarep1gsum2  22564  mdetleib2  22578  mdetfval1  22580  mdet0pr  22582  mdetdiag  22589  mdetdiagid  22590  mdetrlin  22592  mdetrsca  22593  mdetralt  22598  mdetunilem9  22610  gsummatr01  22649  smadiadetlem1a  22653  smadiadetlem3  22658  smadiadetlem4  22659  cpmatmcllem  22708  mat2pmatmul  22721  decpmatmullem  22761  decpmatmul  22762  pmatcollpw1lem2  22765  pmatcollpw  22771  pmatcollpw3lem  22773  pmatcollpwscmat  22781  idpm2idmp  22791  mp2pm2mplem3  22798  mp2pm2mplem4  22799  mp2pm2mplem5  22800  mp2pm2mp  22801  pm2mpghm  22806  pm2mpmhmlem2  22809  monmat2matmon  22814  pm2mp  22815  chpdmat  22831  chpscmat  22832  chpscmatgsumbin  22834  chpscmatgsummon  22835  chp0mat  22836  chpidmat  22837  chfacfscmulgsum  22850  chfacfpmmulgsum  22854  chfacfpmmulgsum2  22855  cayhamlem1  22856  cpmidgsumm2pm  22859  cpmidpmat  22863  cpmadugsumlemB  22864  cpmadugsumlemC  22865  cpmadugsumlemF  22866  cpmadumatpoly  22873  cayhamlem3  22877  cayhamlem4  22878  cayleyhamilton0  22879  cayleyhamiltonALT  22881  neiptopnei  23122  neiptopreu  23123  ptcnplem  23611  cnmpt1t  23655  cnmpt12  23657  cnmptkp  23670  cnmptk1  23671  cnmpt1k  23672  cnmptkk  23673  cnmptk1p  23675  cnmpt2k  23678  qtopeu  23706  pt1hmeo  23796  ptunhmeo  23798  xkocnv  23804  xkohmeo  23805  flfcnp2  23997  cnmpt1plusg  24077  istgp2  24081  tmdmulg  24082  tgpmulg  24083  tmdgsum  24085  subgtgp  24095  symgtgp  24096  tgpconncomp  24103  prdstgpd  24115  tsmsmhm  24136  tsmsadd  24137  tsmssub  24139  tgptsmscls  24140  tsmssplit  24142  tsmsxplem1  24143  tsmsxplem2  24144  cnmpt1vsca  24184  tlmtgp  24186  ustuqtoplem  24229  utopsnneip  24238  ressprdsds  24361  metuval  24539  nmfval0  24580  tngnm  24641  nmoeq0  24726  idnghm  24733  cnmpt1ds  24833  fsumcn  24862  expcn  24864  divccn  24865  divccncf  24898  negcncf  24914  copco  25010  pcopt  25014  pcopt2  25015  pcoass  25016  pi1xfrcnvlem  25048  cnmpt1ip  25239  rrxnm  25383  rrxds  25385  minveclem3b  25420  divcncf  25439  ovolctb  25482  ovoliunnul  25499  voliunlem3  25544  ovolfs2  25563  uniioombllem2  25575  vitalilem4  25603  vitalilem5  25604  ismbf  25620  mbfss  25638  mbfmulc2re  25640  mbfneg  25642  mbfpos  25643  mbfposb  25645  mbfadd  25653  mbfsub  25654  mbfmulc2  25655  mbfinf  25657  mbflimsup  25658  mbflimlem  25659  i1fpos  25698  i1fposd  25699  itg1climres  25706  mbfmul  25718  itg2mulc  25739  itg2i1fseq  25747  itg2cnlem1  25753  itg2cnlem2  25754  itgresr  25771  iblneg  25795  i1fibl  25800  itgitg1  25801  iblsub  25814  itgfsum  25819  itgmulc2lem1  25824  limcmpt  25875  limccnp  25883  limcco  25885  dvreslem  25901  dvres2lem  25902  dvidlem  25907  dvcnp2  25912  dvaddbr  25930  dvmulbr  25931  dvmulf  25935  dvcmulf  25937  dvcobr  25938  dvcof  25940  dvcjbr  25941  dvcj  25942  dvfre  25943  dvexp  25945  dvexp2  25946  dvrec  25947  dvmptcmul  25956  dvmptdivc  25957  dvmptneg  25958  dvmptsub  25959  dvmptre  25961  dvmptim  25962  dvrecg  25965  dvmptdiv  25966  dvmptfsum  25967  dvcnvlem  25968  dvcnv  25969  dvexp3  25970  dvef  25972  dvsincos  25973  dv11cn  25993  lhop2  26007  lhop  26008  ftc2  26036  itgparts  26039  itgsubstlem  26040  mdegfval  26052  mdegmullem  26068  ply1termlem  26193  plypow  26195  plyconst  26196  plyeq0lem  26200  plypf1  26202  plyaddlem1  26203  plymullem1  26204  coeeulem  26214  coeidlem  26227  plyco  26231  coeeq2  26232  0dgr  26235  0dgrb  26236  dgrcolem1  26263  dgrcolem2  26264  plycjlem  26266  dvply1  26275  dvply2g  26276  plydiveu  26289  plyremlem  26295  elqaalem3  26312  taylfval  26349  dvtaylp  26360  taylthlem1  26363  taylthlem2  26364  ulmshft  26380  mtestbdd  26395  iblulm  26397  itgulm2  26399  pserulm  26412  psercn2  26413  pserdvlem2  26418  pserdv  26419  pserdv2  26420  abelthlem1  26421  abelthlem3  26423  advlog  26643  advlogexp  26644  dvcxp1  26729  dvcxp2  26730  dvcncxp1  26732  sqrtcn  26739  loglesqrt  26750  dvatan  26924  atantayl2  26927  atantayl3  26928  leibpi  26931  rlimcnp2  26955  efrlim  26958  dfef2  26959  cxp2lim  26965  divsqrtsumlem  26968  lgamgulmlem2  27018  lgamgulm2  27024  lgamcvglem  27028  gamcvg2lem  27047  ftalem7  27067  basellem9  27077  muinv  27181  logfacrlim  27212  logexprlim  27213  dchrmullid  27240  dchrinvcl  27241  lgseisenlem3  27365  lgseisenlem4  27366  chtppilimlem2  27462  chebbnd2  27465  chpchtlim  27467  chpo1ub  27468  rpvmasumlem  27475  dchrmusumlema  27481  dchrvmasumlem1  27483  dchrvmasumiflem2  27490  dchrisum0fno1  27499  rpvmasum2  27500  dchrisum0lema  27502  dchrisum0lem1  27504  dchrisum0lem2a  27505  dchrisum0lem2  27506  dchrisum0  27508  dchrmusumlem  27510  dchrvmasumlem  27511  rpvmasum  27514  rplogsum  27515  logdivsum  27521  mulog2sumlem3  27524  vmalogdivsum2  27526  vmalogdivsum  27527  2vmadivsumlem  27528  logsqvma2  27531  log2sumbnd  27532  selberglem2  27534  selberg3lem1  27545  selberg3  27547  selberg4lem1  27548  selberg4  27549  pntrsumo1  27553  selberg3r  27557  selberg4r  27558  selberg34r  27559  pntrlog2bndlem2  27566  pntrlog2bndlem4  27568  pntrlog2bndlem5  27569  pntrlog2bndlem6  27571  padicabvf  27619  padicabvcxp  27620  mirval  28748  crctcshlem4  29913  clwlknf1oclwwlkn  30179  eucrct2eupth  30340  chscllem4  31736  brafnmul  32047  kbmul  32051  cofmpt2  32733  ofresid  32741  ofoprabco  32763  fmptunsnop  32799  fcobijfs  32820  fcobijfs2  32821  gsummpt2d  33137  gsummptres  33140  gsummptres2  33141  gsummptf1od  33143  gsummptp1  33145  gsummptfsf1o  33148  gsumfs2d  33149  gsumpart  33151  gsumhashmul  33155  gsummulsubdishift1  33156  gsummulsubdishift2  33157  gsumwrd2dccat  33166  fzto1st1  33190  fzto1st  33191  elrgspnlem1  33330  elrgspnlem2  33331  elrgspnlem3  33332  elrgspnlem4  33333  elrgspnsubrunlem1  33335  elrgspnsubrunlem2  33336  qusbas2  33496  qusima  33498  elrspunidl  33518  elrspunsn  33519  rprmdvdsprod  33624  ressply1evls1  33655  evl1deg1  33666  evl1deg2  33667  evl1deg3  33668  gsummoncoe1fzo  33687  mplasclco  33707  selvply1rhmlemb  33710  selvply1rhmlem2  33712  selvply1rhmlem4  33714  selvply1rhm0  33717  mplmulmvr  33730  evlextv  33733  mplvrpmga  33736  mplvrpmmhm  33737  mplvrpmrhm  33738  psrgsum  33739  psrmonmul  33741  issply  33752  esplyfval0  33755  esplyfval3  33763  esplyfval1  33764  esplyfvaln  33765  esplyind  33766  vietalem  33770  lbsdiflsp0  33817  fedgmullem1  33820  fedgmullem2  33821  fldextrspunlsplem  33864  fldextrspunlsp  33865  extdgfialglem2  33884  mdetpmtr1  34014  mdetlap  34023  xrge0mulc1cn  34132  esumval  34237  esumsnf  34255  esumpcvgval  34269  esumcvg  34277  esumcvgsum  34279  esumsup  34280  ofcfeqd2  34292  meascnbl  34410  sitgval  34523  probmeasb  34621  cndprobprob  34629  dstfrvclim1  34669  ballotlemfval  34681  ballotlemsval  34700  ballotlemieq  34708  plymul02  34737  plymulx0  34738  plymulx  34739  signsplypnf  34741  signstfv  34754  signstfvn  34760  signstfvp  34762  itgexpif  34797  logdivsqrle  34841  ptpconn  35468  cvmliftlem6  35525  cvmliftphtlem  35552  cvmlift3lem5  35558  elmrsubrn  35755  msubfval  35759  msubco  35766  divcnvlin  35968  knoppcnlem9  36814  knoppcnlem10  36815  knoppcnlem11  36816  bj-finsumval0  37652  curf  37972  matunitlindflem1  37990  matunitlindflem2  37991  poimirlem3  37997  poimirlem15  38009  poimirlem16  38010  poimirlem17  38011  poimirlem19  38013  poimirlem20  38014  broucube  38028  ovoliunnfl  38036  voliunnfl  38038  volsupnfl  38039  mbfposadd  38041  itg2addnclem  38045  itg2addnclem3  38047  itg2addnc  38048  itgaddnclem2  38053  itgaddnc  38054  iblsubnc  38055  itgsubnc  38056  itgmulc2nclem1  38060  itgmulc2nclem2  38061  itgmulc2nc  38062  itgabsnc  38063  ftc1cnnclem  38065  ftc1anclem3  38069  ftc1anclem5  38071  ftc1anclem6  38072  ftc1anclem8  38074  ftc1anc  38075  ftc2nc  38076  areacirclem1  38082  areacirclem2  38083  areacirclem4  38085  areacirc  38087  upixp  38103  lcmineqlem8  42528  lcmineqlem12  42532  dvrelog2b  42558  dvrelogpow2b  42560  aks4d1p1p6  42565  aks4d1p1p5  42567  aks6d1c1  42608  aks6d1c5lem3  42629  sticksstones12a  42649  sticksstones12  42650  sticksstones19  42657  aks6d1c6lem1  42662  aks6d1c6lem4  42665  aks6d1c7lem3  42674  qsalrel  42732  rhmcomulpsr  43039  evlselv  43046  fsuppssindlem1  43048  fsuppssind  43050  mhphf  43054  mzpsubst  43204  mzprename  43205  mzpcompact2lem  43207  eldioph2  43218  rabdiophlem2  43254  mendlmod  43641  mendassa  43642  areaquad  43668  fsovcnvlem  44464  hashnzfzclim  44773  expgrowthi  44784  expgrowth  44786  uzmptshftfval  44797  dvradcnv2  44798  binomcxplemrat  44801  binomcxplemfrat  44802  binomcxplemradcnv  44803  binomcxplemdvbinom  44804  binomcxplemcvg  44805  binomcxplemdvsum  44806  binomcxplemnotnn0  44807  mulc1cncfg  46041  expcnfg  46043  fprodcnlem  46051  clim1fr1  46053  divcnvg  46079  sublimc  46102  reclimc  46103  divlimc  46106  limsupresico  46150  limsuppnfdlem  46151  limsupvaluz  46158  supcnvlimsupmpt  46191  liminfresico  46221  climliminflimsupd  46251  cncfmptssg  46321  negcncfg  46331  cncficcgt0  46338  fprodcncf  46350  fprodsubrecnncnvlem  46357  fprodaddrecnncnvlem  46359  dvsinax  46363  dvasinbx  46370  dvdivf  46372  ioodvbdlimc1lem2  46382  ioodvbdlimc2lem  46384  dvnmptdivc  46388  dvxpaek  46390  dvnxpaek  46392  dvnmul  46393  dvnprodlem2  46397  ibliccsinexp  46401  itgsinexplem1  46404  itgsinexp  46405  iblempty  46415  itgcoscmulx  46419  itgsincmulx  46424  itgioocnicc  46427  iblcncfioo  46428  itgsbtaddcnst  46432  volioofmpt  46444  volicofmpt  46447  stoweidlem4  46454  stirlinglem5  46528  dirkerval  46541  dirkertrigeq  46551  dirkeritg  46552  dirkercncflem2  46554  dirkercncflem4  46556  fourierdlem16  46573  fourierdlem18  46575  fourierdlem21  46578  fourierdlem22  46579  fourierdlem28  46585  fourierdlem39  46596  fourierdlem40  46597  fourierdlem41  46598  fourierdlem53  46609  fourierdlem56  46612  fourierdlem57  46613  fourierdlem60  46616  fourierdlem61  46617  fourierdlem68  46624  fourierdlem73  46629  fourierdlem74  46630  fourierdlem75  46631  fourierdlem76  46632  fourierdlem78  46634  fourierdlem81  46637  fourierdlem82  46638  fourierdlem83  46639  fourierdlem84  46640  fourierdlem85  46641  fourierdlem88  46644  fourierdlem90  46646  fourierdlem92  46648  fourierdlem93  46649  fourierdlem95  46651  fourierdlem97  46653  fourierdlem101  46657  fourierdlem103  46659  fourierdlem104  46660  fourierdlem111  46667  fourierdlem112  46668  sqwvfoura  46678  sqwvfourb  46679  fouriersw  46681  elaa2lem  46683  etransclem4  46688  etransclem17  46701  etransclem18  46702  etransclem32  46716  etransclem46  46730  sge0z  46825  sge0revalmpt  46828  sge0tsms  46830  sge0sup  46841  sge0iunmptlemre  46865  sge0iun  46869  sge0xaddlem2  46884  ismeannd  46917  psmeasurelem  46920  meaiuninclem  46930  meaiininclem  46936  caratheodory  46978  isomenndlem  46980  ovnval  46991  hoicvrrex  47006  ovnlecvr  47008  ovncvrrp  47014  ovn0lem  47015  ovnsubaddlem1  47020  hoidmv1lelem2  47042  hoidmv1le  47044  hoidmvlelem3  47047  ovnhoilem2  47052  ovnhoi  47053  ovnlecvr2  47060  ovncvr2  47061  hspmbllem2  47077  ovolval2lem  47093  ovolval3  47097  ovolval5lem1  47102  ovolval5lem2  47103  ovnovollem1  47106  ovnovollem2  47107  vonioolem1  47130  vonicclem1  47133  vonct  47143  smflim  47227  smfinflem  47267  smflimsuplem5  47274  smfliminflem  47280  cfsetsnfsetfv  47527  fundcmpsurbijinjpreimafv  47889  fundcmpsurinjimaid  47893  fdmdifeqresdif  48840  ply1mulgsumlem2  48885  lincvalsc0  48919  linc0scn0  48921  lincdifsn  48922  lincsum  48927  lincscm  48928  lindslinindimp2lem4  48959  lindslinindsimp2lem5  48960  lincresunit3lem2  48978  1arymaptfo  49141  itcovalpclem1  49168  itcovalpclem2  49169  itcovalt2lem1  49173  itcovalt2lem2  49174  tposcurf1  49796  tposcurf2  49797  diag1  49801  fuco22  49836  fucocolem2  49851  fucocolem3  49852  fucocolem4  49853  fucoco  49854  fucolid  49858  fucorid  49859  postcofval  49861  precofval  49864  precofvalALT  49865  precofval2  49866  fucoppcco  49906  islmd  50162  iscmd  50163  aacllem  50298  amgmwlem  50299