Theorem mpteq2dva 5184

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

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1541   ∈ wcel 2111   ↦ cmpt 5172

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-ext 2703

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-sb 2068  df-clab 2710  df-cleq 2723  df-clel 2806  df-opab 5154  df-mpt 5173

This theorem is referenced by:  mpteq2dv  5185  mpteq2ia  5186  2fvcoidd  7231  offval  7619  offval2  7630  coof  7634  caofinvl  7642  caofcom  7647  caofass  7650  caofdi  7652  caofdir  7653  caonncan  7654  curry1  8034  curry2  8037  mpocurryd  8199  pw2f1olem  8994  mapxpen  9056  xpmapenlem  9057  cantnfp1  9571  cantnflem1d  9578  cantnflem1  9579  cnfcom2lem  9591  dfac12lem1  10035  seqof  13966  seqof2  13967  swrdswrd  14612  repswswrd  14691  repswrevw  14694  revco  14741  ccatco  14742  repsco  14747  ofccat  14876  lo1eq  15475  rlimeq  15476  lo1mul2  15536  o1dif  15537  lo1sub  15538  rlimdiv  15553  caucvgr  15583  sumeq1  15596  fsumrlim  15718  fsumo1  15719  climfsum  15727  geomulcvg  15783  vdwlem8  16900  prmgapprmo  16974  restid2  17334  pwsplusgval  17394  pwsmulrval  17395  pwsvscafval  17398  qusin  17448  xpsaddlem  17477  xpsvsca  17481  catidd  17586  fuclid  17876  fucrid  17877  fucass  17878  setcepi  17995  prf1st  18110  prf2nd  18111  1st2ndprf  18112  curfcl  18138  curfuncf  18144  diag2  18151  curf2ndf  18153  hof2val  18162  hofcllem  18164  hofcl  18165  yonedalem4a  18181  yonedalem4c  18183  yonedalem3b  18185  yonedainv  18187  yonffthlem  18188  prdssgrpd  18641  prdsidlem  18677  prdsmndd  18678  mhmvlin  18709  pwsco2mhm  18741  frmdup3lem  18774  frmdup3  18775  smndex1gid  18811  smndex1igid  18812  grpinvpropd  18928  prdsinvlem  18962  pwsinvg  18966  pwssub  18967  galactghm  19317  cayleylem1  19325  pmtrprfval  19400  sylow1lem2  19512  sylow3lem1  19540  efginvrel1  19641  frgpup3lem  19690  frgpup3  19691  prdscmnd  19774  iscyggen  19793  gsumval3  19820  gsumcllem  19821  gsumzsplit  19840  gsumsub  19861  gsummptf1o  19876  gsum2d  19885  gsum2d2  19887  gsumxp  19889  prdsgsum  19894  telgsumfz  19903  telgsumfz0  19905  telgsum  19907  dprdfsub  19936  dprdfeq0  19937  dprddisj2  19954  dprd2d2  19959  dpjidcl  19973  ablfaclem2  20001  ablfac2  20004  prdsmgp  20070  prdsrngd  20095  srgbinomlem3  20147  srgbinomlem4  20148  srgbinomlem  20149  gsumdixp  20238  prdsringd  20240  prdslmodd  20903  mulgrhm2  21416  frgpcyg  21511  freshmansdream  21512  evpmodpmf1o  21534  phlpropd  21593  frlmphl  21719  uvcresum  21731  frlmup1  21736  asclpropd  21835  psrass1lem  21870  psrlinv  21893  psrass1  21902  psrdi  21903  psrdir  21904  psrass23l  21905  psrcom  21906  psrass23  21907  resspsrmul  21914  mplsubrglem  21942  mplmonmul  21972  mplcoe1  21973  mplcoe5  21976  mplcoe4  22007  evlslem3  22016  evlslem1  22018  mhpmulcl  22065  psdmplcl  22078  psdadd  22079  psdmul  22082  psdmvr  22085  psrplusgpropd  22149  psropprmul  22151  coe1mul2  22184  coe1tm  22188  coe1tmmul2  22191  coe1tmmul  22192  coe1pwmul  22194  cply1mul  22212  ply1coe  22214  eqcoe1ply1eq  22215  lply1binomsc  22227  evl1gsummon  22281  evls1fpws  22285  rhmcomulmpl  22298  mamures  22313  grpvrinv  22315  mamuass  22318  mamudi  22319  mamudir  22320  mamuvs1  22321  mamuvs2  22322  mpomatmul  22362  mamutpos  22374  madetsumid  22377  dmatmul  22413  scmatscm  22429  1mavmul  22464  mavmulass  22465  mvmumamul1  22470  mulmarep1gsum1  22489  mulmarep1gsum2  22490  mdetleib2  22504  mdetfval1  22506  mdet0pr  22508  mdetdiag  22515  mdetdiagid  22516  mdetrlin  22518  mdetrsca  22519  mdetralt  22524  mdetunilem9  22536  gsummatr01  22575  smadiadetlem1a  22579  smadiadetlem3  22584  smadiadetlem4  22585  cpmatmcllem  22634  mat2pmatmul  22647  decpmatmullem  22687  decpmatmul  22688  pmatcollpw1lem2  22691  pmatcollpw  22697  pmatcollpw3lem  22699  pmatcollpwscmat  22707  idpm2idmp  22717  mp2pm2mplem3  22724  mp2pm2mplem4  22725  mp2pm2mplem5  22726  mp2pm2mp  22727  pm2mpghm  22732  pm2mpmhmlem2  22735  monmat2matmon  22740  pm2mp  22741  chpdmat  22757  chpscmat  22758  chpscmatgsumbin  22760  chpscmatgsummon  22761  chp0mat  22762  chpidmat  22763  chfacfscmulgsum  22776  chfacfpmmulgsum  22780  chfacfpmmulgsum2  22781  cayhamlem1  22782  cpmidgsumm2pm  22785  cpmidpmat  22789  cpmadugsumlemB  22790  cpmadugsumlemC  22791  cpmadugsumlemF  22792  cpmadumatpoly  22799  cayhamlem3  22803  cayhamlem4  22804  cayleyhamilton0  22805  cayleyhamiltonALT  22807  neiptopnei  23048  neiptopreu  23049  ptcnplem  23537  cnmpt1t  23581  cnmpt12  23583  cnmptkp  23596  cnmptk1  23597  cnmpt1k  23598  cnmptkk  23599  cnmptk1p  23601  cnmpt2k  23604  qtopeu  23632  pt1hmeo  23722  ptunhmeo  23724  xkocnv  23730  xkohmeo  23731  flfcnp2  23923  cnmpt1plusg  24003  istgp2  24007  tmdmulg  24008  tgpmulg  24009  tmdgsum  24011  subgtgp  24021  symgtgp  24022  tgpconncomp  24029  prdstgpd  24041  tsmsmhm  24062  tsmsadd  24063  tsmssub  24065  tgptsmscls  24066  tsmssplit  24068  tsmsxplem1  24069  tsmsxplem2  24070  cnmpt1vsca  24110  tlmtgp  24112  ustuqtoplem  24155  utopsnneip  24164  ressprdsds  24287  metuval  24465  nmfval0  24506  tngnm  24567  nmoeq0  24652  idnghm  24659  cnmpt1ds  24759  fsumcn  24789  expcn  24791  divccn  24792  expcnOLD  24793  divccnOLD  24794  divccncf  24827  negcncf  24843  negcncfOLD  24844  copco  24946  pcopt  24950  pcopt2  24951  pcoass  24952  pi1xfrcnvlem  24984  cnmpt1ip  25175  rrxnm  25319  rrxds  25321  minveclem3b  25356  divcncf  25376  ovolctb  25419  ovoliunnul  25436  voliunlem3  25481  ovolfs2  25500  uniioombllem2  25512  vitalilem4  25540  vitalilem5  25541  ismbf  25557  mbfss  25575  mbfmulc2re  25577  mbfneg  25579  mbfpos  25580  mbfposb  25582  mbfadd  25590  mbfsub  25591  mbfmulc2  25592  mbfinf  25594  mbflimsup  25595  mbflimlem  25596  i1fpos  25635  i1fposd  25636  itg1climres  25643  mbfmul  25655  itg2mulc  25676  itg2i1fseq  25684  itg2cnlem1  25690  itg2cnlem2  25691  itgresr  25708  iblneg  25732  i1fibl  25737  itgitg1  25738  iblsub  25751  itgfsum  25756  itgmulc2lem1  25761  limcmpt  25812  limccnp  25820  limcco  25822  dvreslem  25838  dvres2lem  25839  dvidlem  25844  dvcnp2  25849  dvcnp2OLD  25850  dvaddbr  25868  dvmulbr  25869  dvmulbrOLD  25870  dvmulf  25874  dvcmulf  25876  dvcobr  25877  dvcobrOLD  25878  dvcof  25880  dvcjbr  25881  dvcj  25882  dvfre  25883  dvexp  25885  dvexp2  25886  dvrec  25887  dvmptcmul  25896  dvmptdivc  25897  dvmptneg  25898  dvmptsub  25899  dvmptre  25901  dvmptim  25902  dvrecg  25905  dvmptdiv  25906  dvmptfsum  25907  dvcnvlem  25908  dvcnv  25909  dvexp3  25910  dvef  25912  dvsincos  25913  dv11cn  25934  lhop2  25948  lhop  25949  ftc2  25979  itgparts  25982  itgsubstlem  25983  mdegfval  25995  mdegmullem  26011  ply1termlem  26136  plypow  26138  plyconst  26139  plyeq0lem  26143  plypf1  26145  plyaddlem1  26146  plymullem1  26147  coeeulem  26157  coeidlem  26170  plyco  26174  coeeq2  26175  0dgr  26178  0dgrb  26179  dgrcolem1  26207  dgrcolem2  26208  plycjlem  26210  dvply1  26219  dvply2g  26220  dvply2gOLD  26221  plydiveu  26234  plyremlem  26240  elqaalem3  26257  taylfval  26294  dvtaylp  26306  taylthlem1  26309  taylthlem2  26310  taylthlem2OLD  26311  ulmshft  26327  mtestbdd  26342  iblulm  26344  itgulm2  26346  pserulm  26359  psercn2  26360  psercn2OLD  26361  pserdvlem2  26366  pserdv  26367  pserdv2  26368  abelthlem1  26369  abelthlem3  26371  advlog  26591  advlogexp  26592  dvcxp1  26677  dvcxp2  26678  dvcncxp1  26680  sqrtcn  26688  loglesqrt  26699  dvatan  26873  atantayl2  26876  atantayl3  26877  leibpi  26880  rlimcnp2  26904  efrlim  26907  efrlimOLD  26908  dfef2  26909  cxp2lim  26915  divsqrtsumlem  26918  lgamgulmlem2  26968  lgamgulm2  26974  lgamcvglem  26978  gamcvg2lem  26997  ftalem7  27017  basellem9  27027  muinv  27131  logfacrlim  27163  logexprlim  27164  dchrmullid  27191  dchrinvcl  27192  lgseisenlem3  27316  lgseisenlem4  27317  chtppilimlem2  27413  chebbnd2  27416  chpchtlim  27418  chpo1ub  27419  rpvmasumlem  27426  dchrmusumlema  27432  dchrvmasumlem1  27434  dchrvmasumiflem2  27441  dchrisum0fno1  27450  rpvmasum2  27451  dchrisum0lema  27453  dchrisum0lem1  27455  dchrisum0lem2a  27456  dchrisum0lem2  27457  dchrisum0  27459  dchrmusumlem  27461  dchrvmasumlem  27462  rpvmasum  27465  rplogsum  27466  logdivsum  27472  mulog2sumlem3  27475  vmalogdivsum2  27477  vmalogdivsum  27478  2vmadivsumlem  27479  logsqvma2  27482  log2sumbnd  27483  selberglem2  27485  selberg3lem1  27496  selberg3  27498  selberg4lem1  27499  selberg4  27500  pntrsumo1  27504  selberg3r  27508  selberg4r  27509  selberg34r  27510  pntrlog2bndlem2  27517  pntrlog2bndlem4  27519  pntrlog2bndlem5  27520  pntrlog2bndlem6  27522  padicabvf  27570  padicabvcxp  27571  mirval  28634  crctcshlem4  29799  clwlknf1oclwwlkn  30062  eucrct2eupth  30223  chscllem4  31618  brafnmul  31929  kbmul  31933  cofmpt2  32614  ofresid  32622  ofoprabco  32644  fmptunsnop  32679  fcobijfs  32702  fcobijfs2  32703  gsummpt2d  33027  gsummptres  33030  gsummptres2  33031  gsummptfsf1o  33032  gsumfs2d  33033  gsumpart  33035  gsumhashmul  33039  gsumwrd2dccat  33045  fzto1st1  33069  fzto1st  33070  elrgspnlem1  33207  elrgspnlem2  33208  elrgspnlem3  33209  elrgspnlem4  33210  elrgspnsubrunlem1  33212  elrgspnsubrunlem2  33213  qusbas2  33369  qusima  33371  elrspunidl  33391  elrspunsn  33392  rprmdvdsprod  33497  ressply1evls1  33526  evl1deg1  33537  evl1deg2  33538  evl1deg3  33539  gsummoncoe1fzo  33556  mplvrpmga  33573  mplvrpmmhm  33574  mplvrpmrhm  33575  issply  33582  lbsdiflsp0  33637  fedgmullem1  33640  fedgmullem2  33641  fldextrspunlsplem  33684  fldextrspunlsp  33685  extdgfialglem2  33704  mdetpmtr1  33834  mdetlap  33843  xrge0mulc1cn  33952  esumval  34057  esumsnf  34075  esumpcvgval  34089  esumcvg  34097  esumcvgsum  34099  esumsup  34100  ofcfeqd2  34112  meascnbl  34230  sitgval  34343  probmeasb  34441  cndprobprob  34449  dstfrvclim1  34489  ballotlemfval  34501  ballotlemsval  34520  ballotlemieq  34528  plymul02  34557  plymulx0  34558  plymulx  34559  signsplypnf  34561  signstfv  34574  signstfvn  34580  signstfvp  34582  itgexpif  34617  logdivsqrle  34661  ptpconn  35275  cvmliftlem6  35332  cvmliftphtlem  35359  cvmlift3lem5  35365  elmrsubrn  35562  msubfval  35566  msubco  35573  divcnvlin  35775  knoppcnlem9  36541  knoppcnlem10  36542  knoppcnlem11  36543  bj-finsumval0  37325  curf  37644  matunitlindflem1  37662  matunitlindflem2  37663  poimirlem3  37669  poimirlem15  37681  poimirlem16  37682  poimirlem17  37683  poimirlem19  37685  poimirlem20  37686  broucube  37700  ovoliunnfl  37708  voliunnfl  37710  volsupnfl  37711  mbfposadd  37713  itg2addnclem  37717  itg2addnclem3  37719  itg2addnc  37720  itgaddnclem2  37725  itgaddnc  37726  iblsubnc  37727  itgsubnc  37728  itgmulc2nclem1  37732  itgmulc2nclem2  37733  itgmulc2nc  37734  itgabsnc  37735  ftc1cnnclem  37737  ftc1anclem3  37741  ftc1anclem5  37743  ftc1anclem6  37744  ftc1anclem8  37746  ftc1anc  37747  ftc2nc  37748  areacirclem1  37754  areacirclem2  37755  areacirclem4  37757  areacirc  37759  upixp  37775  lcmineqlem8  42075  lcmineqlem12  42079  dvrelog2b  42105  dvrelogpow2b  42107  aks4d1p1p6  42112  aks4d1p1p5  42114  aks6d1c1  42155  aks6d1c5lem3  42176  sticksstones12a  42196  sticksstones12  42197  sticksstones19  42204  aks6d1c6lem1  42209  aks6d1c6lem4  42212  aks6d1c7lem3  42221  qsalrel  42279  pwsgprod  42583  rhmcomulpsr  42590  evlsvvval  42602  evlsevl  42610  selvvvval  42624  evlselv  42626  fsuppssindlem1  42630  fsuppssind  42632  mhphf  42636  mzpsubst  42787  mzprename  42788  mzpcompact2lem  42790  eldioph2  42801  rabdiophlem2  42841  mendlmod  43228  mendassa  43229  areaquad  43255  fsovcnvlem  44052  hashnzfzclim  44361  expgrowthi  44372  expgrowth  44374  uzmptshftfval  44385  dvradcnv2  44386  binomcxplemrat  44389  binomcxplemfrat  44390  binomcxplemradcnv  44391  binomcxplemdvbinom  44392  binomcxplemcvg  44393  binomcxplemdvsum  44394  binomcxplemnotnn0  44395  mulc1cncfg  45635  expcnfg  45637  fprodcnlem  45645  clim1fr1  45647  divcnvg  45673  sublimc  45696  reclimc  45697  divlimc  45700  limsupresico  45744  limsuppnfdlem  45745  limsupvaluz  45752  supcnvlimsupmpt  45785  liminfresico  45815  climliminflimsupd  45845  cncfmptssg  45915  negcncfg  45925  cncficcgt0  45932  fprodcncf  45944  fprodsubrecnncnvlem  45951  fprodaddrecnncnvlem  45953  dvsinax  45957  dvasinbx  45964  dvdivf  45966  ioodvbdlimc1lem2  45976  ioodvbdlimc2lem  45978  dvnmptdivc  45982  dvxpaek  45984  dvnxpaek  45986  dvnmul  45987  dvnprodlem2  45991  ibliccsinexp  45995  itgsinexplem1  45998  itgsinexp  45999  iblempty  46009  itgcoscmulx  46013  itgsincmulx  46018  itgioocnicc  46021  iblcncfioo  46022  itgsbtaddcnst  46026  volioofmpt  46038  volicofmpt  46041  stoweidlem4  46048  stirlinglem5  46122  dirkerval  46135  dirkertrigeq  46145  dirkeritg  46146  dirkercncflem2  46148  dirkercncflem4  46150  fourierdlem16  46167  fourierdlem18  46169  fourierdlem21  46172  fourierdlem22  46173  fourierdlem28  46179  fourierdlem39  46190  fourierdlem40  46191  fourierdlem41  46192  fourierdlem53  46203  fourierdlem56  46206  fourierdlem57  46207  fourierdlem60  46210  fourierdlem61  46211  fourierdlem68  46218  fourierdlem73  46223  fourierdlem74  46224  fourierdlem75  46225  fourierdlem76  46226  fourierdlem78  46228  fourierdlem81  46231  fourierdlem82  46232  fourierdlem83  46233  fourierdlem84  46234  fourierdlem85  46235  fourierdlem88  46238  fourierdlem90  46240  fourierdlem92  46242  fourierdlem93  46243  fourierdlem95  46245  fourierdlem97  46247  fourierdlem101  46251  fourierdlem103  46253  fourierdlem104  46254  fourierdlem111  46261  fourierdlem112  46262  sqwvfoura  46272  sqwvfourb  46273  fouriersw  46275  elaa2lem  46277  etransclem4  46282  etransclem17  46295  etransclem18  46296  etransclem32  46310  etransclem46  46324  sge0z  46419  sge0revalmpt  46422  sge0tsms  46424  sge0sup  46435  sge0iunmptlemre  46459  sge0iun  46463  sge0xaddlem2  46478  ismeannd  46511  psmeasurelem  46514  meaiuninclem  46524  meaiininclem  46530  caratheodory  46572  isomenndlem  46574  ovnval  46585  hoicvrrex  46600  ovnlecvr  46602  ovncvrrp  46608  ovn0lem  46609  ovnsubaddlem1  46614  hoidmv1lelem2  46636  hoidmv1le  46638  hoidmvlelem3  46641  ovnhoilem2  46646  ovnhoi  46647  ovnlecvr2  46654  ovncvr2  46655  hspmbllem2  46671  ovolval2lem  46687  ovolval3  46691  ovolval5lem1  46696  ovolval5lem2  46697  ovnovollem1  46700  ovnovollem2  46701  vonioolem1  46724  vonicclem1  46727  vonct  46737  smflim  46821  smfinflem  46861  smflimsuplem5  46868  smfliminflem  46874  cfsetsnfsetfv  47094  fundcmpsurbijinjpreimafv  47444  fundcmpsurinjimaid  47448  fdmdifeqresdif  48379  ply1mulgsumlem2  48425  lincvalsc0  48459  linc0scn0  48461  lincdifsn  48462  lincsum  48467  lincscm  48468  lindslinindimp2lem4  48499  lindslinindsimp2lem5  48500  lincresunit3lem2  48518  1arymaptfo  48681  itcovalpclem1  48708  itcovalpclem2  48709  itcovalt2lem1  48713  itcovalt2lem2  48714  tposcurf1  49337  tposcurf2  49338  diag1  49342  fuco22  49377  fucocolem2  49392  fucocolem3  49393  fucocolem4  49394  fucoco  49395  fucolid  49399  fucorid  49400  postcofval  49402  precofval  49405  precofvalALT  49406  precofval2  49407  fucoppcco  49447  islmd  49703  iscmd  49704  aacllem  49839  amgmwlem  49840