Theorem mpteq2dva 5247

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

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1536   ∈ wcel 2105   ↦ cmpt 5230

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1776  df-sb 2062  df-clab 2712  df-cleq 2726  df-clel 2813  df-opab 5210  df-mpt 5231

This theorem is referenced by:  mpteq2dv  5249  mpteq2ia  5250  2fvcoidd  7316  offval  7705  offval2  7716  coof  7720  caofinvl  7728  caofcom  7733  caofass  7735  caofdi  7737  caofdir  7738  caonncan  7739  curry1  8127  curry2  8130  mpocurryd  8292  pw2f1olem  9114  mapxpen  9181  xpmapenlem  9182  cantnfp1  9718  cantnflem1d  9725  cantnflem1  9726  cnfcom2lem  9738  dfac12lem1  10181  seqof  14096  seqof2  14097  swrdswrd  14739  repswswrd  14818  repswrevw  14821  revco  14869  ccatco  14870  repsco  14875  ofccat  15004  lo1eq  15600  rlimeq  15601  lo1mul2  15661  o1dif  15662  lo1sub  15663  rlimdiv  15678  caucvgr  15708  sumeq1  15721  fsumrlim  15843  fsumo1  15844  climfsum  15852  geomulcvg  15908  vdwlem8  17021  prmgapprmo  17095  restid2  17476  pwsplusgval  17536  pwsmulrval  17537  pwsvscafval  17540  qusin  17590  xpsaddlem  17619  xpsvsca  17623  catidd  17724  fuclid  18022  fucrid  18023  fucass  18024  setcepi  18141  prf1st  18259  prf2nd  18260  1st2ndprf  18261  curfcl  18288  curfuncf  18294  diag2  18301  curf2ndf  18303  hof2val  18312  hofcllem  18314  hofcl  18315  yonedalem4a  18331  yonedalem4c  18333  yonedalem3b  18335  yonedainv  18337  yonffthlem  18338  prdssgrpd  18758  prdsidlem  18794  prdsmndd  18795  mhmvlin  18826  pwsco2mhm  18858  frmdup3lem  18891  frmdup3  18892  smndex1gid  18928  smndex1igid  18929  grpinvpropd  19045  prdsinvlem  19079  pwsinvg  19083  pwssub  19084  galactghm  19436  cayleylem1  19444  pmtrprfval  19519  sylow1lem2  19631  sylow3lem1  19659  efginvrel1  19760  frgpup3lem  19809  frgpup3  19810  prdscmnd  19893  iscyggen  19912  gsumval3  19939  gsumcllem  19940  gsumzsplit  19959  gsumsub  19980  gsummptf1o  19995  gsum2d  20004  gsum2d2  20006  gsumxp  20008  prdsgsum  20013  telgsumfz  20022  telgsumfz0  20024  telgsum  20026  dprdfsub  20055  dprdfeq0  20056  dprddisj2  20073  dprd2d2  20078  dpjidcl  20092  ablfaclem2  20120  ablfac2  20123  prdsmgp  20168  prdsrngd  20193  srgbinomlem3  20245  srgbinomlem4  20246  srgbinomlem  20247  gsumdixp  20332  prdsringd  20334  prdslmodd  20984  mulgrhm2  21506  frgpcyg  21609  freshmansdream  21610  evpmodpmf1o  21631  phlpropd  21690  frlmphl  21818  uvcresum  21830  frlmup1  21835  asclpropd  21934  psrass1lem  21969  psrlinv  21992  psrass1  22001  psrdi  22002  psrdir  22003  psrass23l  22004  psrcom  22005  psrass23  22006  resspsrmul  22013  mplsubrglem  22041  mplmonmul  22071  mplcoe1  22072  mplcoe5  22075  mplcoe4  22112  evlslem3  22121  evlslem1  22123  mhpmulcl  22170  psdmplcl  22183  psdadd  22184  psdmul  22187  psrplusgpropd  22252  psropprmul  22254  coe1mul2  22287  coe1tm  22291  coe1tmmul2  22294  coe1tmmul  22295  coe1pwmul  22297  cply1mul  22315  ply1coe  22317  eqcoe1ply1eq  22318  lply1binomsc  22330  evl1gsummon  22384  evls1fpws  22388  rhmcomulmpl  22401  mamures  22416  grpvrinv  22418  mamuass  22421  mamudi  22422  mamudir  22423  mamuvs1  22424  mamuvs2  22425  mpomatmul  22467  mamutpos  22479  madetsumid  22482  dmatmul  22518  scmatscm  22534  1mavmul  22569  mavmulass  22570  mvmumamul1  22575  mulmarep1gsum1  22594  mulmarep1gsum2  22595  mdetleib2  22609  mdetfval1  22611  mdet0pr  22613  mdetdiag  22620  mdetdiagid  22621  mdetrlin  22623  mdetrsca  22624  mdetralt  22629  mdetunilem9  22641  gsummatr01  22680  smadiadetlem1a  22684  smadiadetlem3  22689  smadiadetlem4  22690  cpmatmcllem  22739  mat2pmatmul  22752  decpmatmullem  22792  decpmatmul  22793  pmatcollpw1lem2  22796  pmatcollpw  22802  pmatcollpw3lem  22804  pmatcollpwscmat  22812  idpm2idmp  22822  mp2pm2mplem3  22829  mp2pm2mplem4  22830  mp2pm2mplem5  22831  mp2pm2mp  22832  pm2mpghm  22837  pm2mpmhmlem2  22840  monmat2matmon  22845  pm2mp  22846  chpdmat  22862  chpscmat  22863  chpscmatgsumbin  22865  chpscmatgsummon  22866  chp0mat  22867  chpidmat  22868  chfacfscmulgsum  22881  chfacfpmmulgsum  22885  chfacfpmmulgsum2  22886  cayhamlem1  22887  cpmidgsumm2pm  22890  cpmidpmat  22894  cpmadugsumlemB  22895  cpmadugsumlemC  22896  cpmadugsumlemF  22897  cpmadumatpoly  22904  cayhamlem3  22908  cayhamlem4  22909  cayleyhamilton0  22910  cayleyhamiltonALT  22912  neiptopnei  23155  neiptopreu  23156  ptcnplem  23644  cnmpt1t  23688  cnmpt12  23690  cnmptkp  23703  cnmptk1  23704  cnmpt1k  23705  cnmptkk  23706  cnmptk1p  23708  cnmpt2k  23711  qtopeu  23739  pt1hmeo  23829  ptunhmeo  23831  xkocnv  23837  xkohmeo  23838  flfcnp2  24030  cnmpt1plusg  24110  istgp2  24114  tmdmulg  24115  tgpmulg  24116  tmdgsum  24118  subgtgp  24128  symgtgp  24129  tgpconncomp  24136  prdstgpd  24148  tsmsmhm  24169  tsmsadd  24170  tsmssub  24172  tgptsmscls  24173  tsmssplit  24175  tsmsxplem1  24176  tsmsxplem2  24177  cnmpt1vsca  24217  tlmtgp  24219  ustuqtoplem  24263  utopsnneip  24272  ressprdsds  24396  metuval  24577  nmfval0  24618  tngnm  24687  nmoeq0  24772  idnghm  24779  cnmpt1ds  24877  fsumcn  24907  expcn  24909  divccn  24910  expcnOLD  24911  divccnOLD  24912  divccncf  24945  negcncf  24961  negcncfOLD  24962  copco  25064  pcopt  25068  pcopt2  25069  pcoass  25070  pi1xfrcnvlem  25102  cnmpt1ip  25294  rrxnm  25438  rrxds  25440  minveclem3b  25475  divcncf  25495  ovolctb  25538  ovoliunnul  25555  voliunlem3  25600  ovolfs2  25619  uniioombllem2  25631  vitalilem4  25659  vitalilem5  25660  ismbf  25676  mbfss  25694  mbfmulc2re  25696  mbfneg  25698  mbfpos  25699  mbfposb  25701  mbfadd  25709  mbfsub  25710  mbfmulc2  25711  mbfinf  25713  mbflimsup  25714  mbflimlem  25715  i1fpos  25755  i1fposd  25756  itg1climres  25763  mbfmul  25775  itg2mulc  25796  itg2i1fseq  25804  itg2cnlem1  25810  itg2cnlem2  25811  itgresr  25828  iblneg  25852  i1fibl  25857  itgitg1  25858  iblsub  25871  itgfsum  25876  itgmulc2lem1  25881  limcmpt  25932  limccnp  25940  limcco  25942  dvreslem  25958  dvres2lem  25959  dvidlem  25964  dvcnp2  25969  dvcnp2OLD  25970  dvaddbr  25988  dvmulbr  25989  dvmulbrOLD  25990  dvmulf  25994  dvcmulf  25996  dvcobr  25997  dvcobrOLD  25998  dvcof  26000  dvcjbr  26001  dvcj  26002  dvfre  26003  dvexp  26005  dvexp2  26006  dvrec  26007  dvmptcmul  26016  dvmptdivc  26017  dvmptneg  26018  dvmptsub  26019  dvmptre  26021  dvmptim  26022  dvrecg  26025  dvmptdiv  26026  dvmptfsum  26027  dvcnvlem  26028  dvcnv  26029  dvexp3  26030  dvef  26032  dvsincos  26033  dv11cn  26054  lhop2  26068  lhop  26069  ftc2  26099  itgparts  26102  itgsubstlem  26103  mdegfval  26115  mdegmullem  26131  ply1termlem  26256  plypow  26258  plyconst  26259  plyeq0lem  26263  plypf1  26265  plyaddlem1  26266  plymullem1  26267  coeeulem  26277  coeidlem  26290  plyco  26294  coeeq2  26295  0dgr  26298  0dgrb  26299  dgrcolem1  26327  dgrcolem2  26328  plycjlem  26330  dvply1  26339  dvply2g  26340  dvply2gOLD  26341  plydiveu  26354  plyremlem  26360  elqaalem3  26377  taylfval  26414  dvtaylp  26426  taylthlem1  26429  taylthlem2  26430  taylthlem2OLD  26431  ulmshft  26447  mtestbdd  26462  iblulm  26464  itgulm2  26466  pserulm  26479  psercn2  26480  psercn2OLD  26481  pserdvlem2  26486  pserdv  26487  pserdv2  26488  abelthlem1  26489  abelthlem3  26491  advlog  26710  advlogexp  26711  dvcxp1  26796  dvcxp2  26797  dvcncxp1  26799  sqrtcn  26807  loglesqrt  26818  dvatan  26992  atantayl2  26995  atantayl3  26996  leibpi  26999  rlimcnp2  27023  efrlim  27026  efrlimOLD  27027  dfef2  27028  cxp2lim  27034  divsqrtsumlem  27037  lgamgulmlem2  27087  lgamgulm2  27093  lgamcvglem  27097  gamcvg2lem  27116  ftalem7  27136  basellem9  27146  muinv  27250  logfacrlim  27282  logexprlim  27283  dchrmullid  27310  dchrinvcl  27311  lgseisenlem3  27435  lgseisenlem4  27436  chtppilimlem2  27532  chebbnd2  27535  chpchtlim  27537  chpo1ub  27538  rpvmasumlem  27545  dchrmusumlema  27551  dchrvmasumlem1  27553  dchrvmasumiflem2  27560  dchrisum0fno1  27569  rpvmasum2  27570  dchrisum0lema  27572  dchrisum0lem1  27574  dchrisum0lem2a  27575  dchrisum0lem2  27576  dchrisum0  27578  dchrmusumlem  27580  dchrvmasumlem  27581  rpvmasum  27584  rplogsum  27585  logdivsum  27591  mulog2sumlem3  27594  vmalogdivsum2  27596  vmalogdivsum  27597  2vmadivsumlem  27598  logsqvma2  27601  log2sumbnd  27602  selberglem2  27604  selberg3lem1  27615  selberg3  27617  selberg4lem1  27618  selberg4  27619  pntrsumo1  27623  selberg3r  27627  selberg4r  27628  selberg34r  27629  pntrlog2bndlem2  27636  pntrlog2bndlem4  27638  pntrlog2bndlem5  27639  pntrlog2bndlem6  27641  padicabvf  27689  padicabvcxp  27690  mirval  28677  crctcshlem4  29849  clwlknf1oclwwlkn  30112  eucrct2eupth  30273  chscllem4  31668  brafnmul  31979  kbmul  31983  cofmpt2  32650  ofresid  32658  ofoprabco  32680  fmptunsnop  32714  fcobijfs  32740  gsummpt2d  33034  gsummptres  33037  gsummptres2  33038  gsummptfsf1o  33039  gsumfs2d  33040  gsumpart  33042  gsumhashmul  33046  gsumwrd2dccat  33052  fzto1st1  33104  fzto1st  33105  elrgspnlem1  33231  elrgspnlem2  33232  elrgspnlem3  33233  elrgspnlem4  33234  qusbas2  33413  qusima  33415  elrspunidl  33435  elrspunsn  33436  rprmdvdsprod  33541  evl1deg1  33580  evl1deg2  33581  evl1deg3  33582  gsummoncoe1fzo  33597  lbsdiflsp0  33653  fedgmullem1  33656  fedgmullem2  33657  mdetpmtr1  33783  mdetlap  33792  xrge0mulc1cn  33901  esumval  34026  esumsnf  34044  esumpcvgval  34058  esumcvg  34066  esumcvgsum  34068  esumsup  34069  ofcfeqd2  34081  meascnbl  34199  sitgval  34313  probmeasb  34411  cndprobprob  34419  dstfrvclim1  34458  ballotlemfval  34470  ballotlemsval  34489  ballotlemieq  34497  plymul02  34539  plymulx0  34540  plymulx  34541  signsplypnf  34543  signstfv  34556  signstfvn  34562  signstfvp  34564  itgexpif  34599  logdivsqrle  34643  ptpconn  35217  cvmliftlem6  35274  cvmliftphtlem  35301  cvmlift3lem5  35307  elmrsubrn  35504  msubfval  35508  msubco  35515  divcnvlin  35712  knoppcnlem9  36483  knoppcnlem10  36484  knoppcnlem11  36485  bj-finsumval0  37267  curf  37584  matunitlindflem1  37602  matunitlindflem2  37603  poimirlem3  37609  poimirlem15  37621  poimirlem16  37622  poimirlem17  37623  poimirlem19  37625  poimirlem20  37626  broucube  37640  ovoliunnfl  37648  voliunnfl  37650  volsupnfl  37651  mbfposadd  37653  itg2addnclem  37657  itg2addnclem3  37659  itg2addnc  37660  itgaddnclem2  37665  itgaddnc  37666  iblsubnc  37667  itgsubnc  37668  itgmulc2nclem1  37672  itgmulc2nclem2  37673  itgmulc2nc  37674  itgabsnc  37675  ftc1cnnclem  37677  ftc1anclem3  37681  ftc1anclem5  37683  ftc1anclem6  37684  ftc1anclem8  37686  ftc1anc  37687  ftc2nc  37688  areacirclem1  37694  areacirclem2  37695  areacirclem4  37697  areacirc  37699  upixp  37715  lcmineqlem8  42017  lcmineqlem12  42021  dvrelog2b  42047  dvrelogpow2b  42049  aks4d1p1p6  42054  aks4d1p1p5  42056  aks6d1c1  42097  aks6d1c5lem3  42118  sticksstones12a  42138  sticksstones12  42139  sticksstones19  42146  aks6d1c6lem1  42151  aks6d1c6lem4  42154  aks6d1c7lem3  42163  qsalrel  42259  pwsgprod  42530  rhmcomulpsr  42537  evlsvvval  42549  evlsevl  42557  selvvvval  42571  evlselv  42573  fsuppssindlem1  42577  fsuppssind  42579  mhphf  42583  mzpsubst  42735  mzprename  42736  mzpcompact2lem  42738  eldioph2  42749  rabdiophlem2  42789  mendlmod  43177  mendassa  43178  areaquad  43204  fsovcnvlem  44002  hashnzfzclim  44317  expgrowthi  44328  expgrowth  44330  uzmptshftfval  44341  dvradcnv2  44342  binomcxplemrat  44345  binomcxplemfrat  44346  binomcxplemradcnv  44347  binomcxplemdvbinom  44348  binomcxplemcvg  44349  binomcxplemdvsum  44350  binomcxplemnotnn0  44351  mulc1cncfg  45544  expcnfg  45546  fprodcnlem  45554  clim1fr1  45556  divcnvg  45582  sublimc  45607  reclimc  45608  divlimc  45611  limsupresico  45655  limsuppnfdlem  45656  limsupvaluz  45663  supcnvlimsupmpt  45696  liminfresico  45726  climliminflimsupd  45756  cncfmptssg  45826  negcncfg  45836  cncficcgt0  45843  fprodcncf  45855  fprodsubrecnncnvlem  45862  fprodaddrecnncnvlem  45864  dvsinax  45868  dvasinbx  45875  dvdivf  45877  ioodvbdlimc1lem2  45887  ioodvbdlimc2lem  45889  dvnmptdivc  45893  dvxpaek  45895  dvnxpaek  45897  dvnmul  45898  dvnprodlem2  45902  ibliccsinexp  45906  itgsinexplem1  45909  itgsinexp  45910  iblempty  45920  itgcoscmulx  45924  itgsincmulx  45929  itgioocnicc  45932  iblcncfioo  45933  itgsbtaddcnst  45937  volioofmpt  45949  volicofmpt  45952  stoweidlem4  45959  stirlinglem5  46033  dirkerval  46046  dirkertrigeq  46056  dirkeritg  46057  dirkercncflem2  46059  dirkercncflem4  46061  fourierdlem16  46078  fourierdlem18  46080  fourierdlem21  46083  fourierdlem22  46084  fourierdlem28  46090  fourierdlem39  46101  fourierdlem40  46102  fourierdlem41  46103  fourierdlem53  46114  fourierdlem56  46117  fourierdlem57  46118  fourierdlem60  46121  fourierdlem61  46122  fourierdlem68  46129  fourierdlem73  46134  fourierdlem74  46135  fourierdlem75  46136  fourierdlem76  46137  fourierdlem78  46139  fourierdlem81  46142  fourierdlem82  46143  fourierdlem83  46144  fourierdlem84  46145  fourierdlem85  46146  fourierdlem88  46149  fourierdlem90  46151  fourierdlem92  46153  fourierdlem93  46154  fourierdlem95  46156  fourierdlem97  46158  fourierdlem101  46162  fourierdlem103  46164  fourierdlem104  46165  fourierdlem111  46172  fourierdlem112  46173  sqwvfoura  46183  sqwvfourb  46184  fouriersw  46186  elaa2lem  46188  etransclem4  46193  etransclem17  46206  etransclem18  46207  etransclem32  46221  etransclem46  46235  sge0z  46330  sge0revalmpt  46333  sge0tsms  46335  sge0sup  46346  sge0iunmptlemre  46370  sge0iun  46374  sge0xaddlem2  46389  ismeannd  46422  psmeasurelem  46425  meaiuninclem  46435  meaiininclem  46441  caratheodory  46483  isomenndlem  46485  ovnval  46496  hoicvrrex  46511  ovnlecvr  46513  ovncvrrp  46519  ovn0lem  46520  ovnsubaddlem1  46525  hoidmv1lelem2  46547  hoidmv1le  46549  hoidmvlelem3  46552  ovnhoilem2  46557  ovnhoi  46558  ovnlecvr2  46565  ovncvr2  46566  hspmbllem2  46582  ovolval2lem  46598  ovolval3  46602  ovolval5lem1  46607  ovolval5lem2  46608  ovnovollem1  46611  ovnovollem2  46612  vonioolem1  46635  vonicclem1  46638  vonct  46648  smflim  46732  smfinflem  46772  smflimsuplem5  46779  smfliminflem  46785  cfsetsnfsetfv  47006  fundcmpsurbijinjpreimafv  47331  fundcmpsurinjimaid  47335  fdmdifeqresdif  48186  ply1mulgsumlem2  48232  lincvalsc0  48266  linc0scn0  48268  lincdifsn  48269  lincsum  48274  lincscm  48275  lindslinindimp2lem4  48306  lindslinindsimp2lem5  48307  lincresunit3lem2  48325  1arymaptfo  48492  itcovalpclem1  48519  itcovalpclem2  48520  itcovalt2lem1  48524  itcovalt2lem2  48525  aacllem  49031  amgmwlem  49032