Theorem mpteq2dva 5202

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

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

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 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-sb 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-opab 5172  df-mpt 5191

This theorem is used by:  mpteq2dv  5203  mpteq2ia  5204  2fvcoidd  7334  offval  7732  offval2  7743  coof  7747  caofinvl  7755  caofcom  7760  caofass  7763  caofdi  7765  caofdir  7766  caonncan  7767  curry1  8150  curry2  8153  mpocurryd  8322  curf  8926  pw2f1olem  9136  mapxpen  9198  xpmapenlem  9199  cantnfp1  9717  cantnflem1d  9724  cantnflem1  9725  cnfcom2lem  9737  dfac12lem1  10259  seqof  14240  seqof2  14241  swrdswrd  14894  repswswrd  14975  repswrevw  14978  revco  15025  ccatco  15026  repsco  15031  ofccat  15163  lo1eq  15776  rlimeq  15777  lo1mul2  15837  o1dif  15838  lo1sub  15839  rlimdiv  15854  caucvgr  15884  sumeq1  15897  fsumrlim  16019  fsumo1  16020  climfsum  16028  geomulcvg  16086  vdwlem8  17207  prmgapprmo  17281  restid2  17642  pwsplusgval  17703  pwsmulrval  17704  pwsvscafval  17707  qusin  17757  xpsaddlem  17786  xpsvsca  17790  catidd  17895  fuclid  18185  fucrid  18186  fucass  18187  setcepi  18304  prf1st  18419  prf2nd  18420  1st2ndprf  18421  curfcl  18447  curfuncf  18453  diag2  18460  curf2ndf  18462  hof2val  18471  hofcllem  18473  hofcl  18474  yonedalem4a  18490  yonedalem4c  18492  yonedalem3b  18494  yonedainv  18496  yonffthlem  18497  prdssgrpd  18963  prdsidlem  19004  prdsmndd  19005  mhmvlin  19037  pwsco2mhm  19070  frmdup3lem  19103  frmdup3  19104  smndex1gid  19141  smndex1gidOLD  19142  smndex1igidOLD  19144  grpinvpropd  19266  prdsinvlem  19300  pwsinvg  19304  pwssub  19305  galactghm  19660  cayleylem1  19668  pmtrprfval  19743  sylow1lem2  19855  sylow3lem1  19883  efginvrel1  19984  frgpup3lem  20033  frgpup3  20034  prdscmnd  20117  iscyggen  20136  gsumval3  20163  gsumcllem  20164  gsumzsplit  20183  gsumsub  20204  gsummptf1o  20219  gsum2d  20228  gsum2d2  20230  gsumxp  20232  prdsgsum  20237  telgsumfz  20246  telgsumfz0  20248  telgsum  20250  dprdfsub  20279  dprdfeq0  20280  dprddisj2  20297  dprd2d2  20302  dpjidcl  20316  ablfaclem2  20344  ablfac2  20347  prdsmgp  20413  prdsrngd  20440  srgbinomlem3  20496  srgbinomlem4  20497  srgbinomlem  20498  gsumdixp  20590  prdsringd  20592  pwsgprod  20601  prdslmodd  21286  mulgrhm2  21828  frgpcyg  21923  freshmansdream  21924  evpmodpmf1o  21946  phlpropd  22005  frlmphl  22131  uvcresum  22143  frlmup1  22148  asclpropd  22249  psrass1lem  22285  psrlinv  22307  psrass1  22315  psrdi  22316  psrdir  22317  psrass23l  22318  psrcom  22319  psrass23  22320  resspsrmul  22327  mplsubrglem  22355  mplmonmul  22389  mplcoe1  22390  mplcoe5  22393  mplcoe4  22424  evlslem3  22433  evlslem1  22435  evlsvvval  22446  rhmcomulmpl  22477  evlsevl  22485  selvvvval  22495  mhpmulcl  22514  psdmplcl  22527  psdadd  22528  psdmul  22531  psdmvr  22534  psrplusgpropd  22597  psropprmul  22599  coe1mul2  22632  coe1tm  22636  coe1tmmul2  22639  coe1tmmul  22640  coe1pwmul  22642  cply1mul  22658  ply1coe  22660  eqcoe1ply1eq  22661  lply1binomsc  22673  evl1gsummon  22727  evls1fpws  22731  mamures  22756  grpvrinv  22758  mamuass  22761  mamudi  22762  mamudir  22763  mamuvs1  22764  mamuvs2  22765  mpomatmul  22805  mamutpos  22817  madetsumid  22820  dmatmul  22856  scmatscm  22872  1mavmul  22907  mavmulass  22908  mvmumamul1  22913  mulmarep1gsum1  22932  mulmarep1gsum2  22933  mdetleib2  22947  mdetfval1  22949  mdet0pr  22951  mdetdiag  22958  mdetdiagid  22959  mdetrlin  22961  mdetrsca  22962  mdetralt  22967  mdetunilem9  22979  gsummatr01  23018  smadiadetlem1a  23022  smadiadetlem3  23027  smadiadetlem4  23028  matunitlindflem1  23038  matunitlindflem2  23039  cpmatmcllem  23080  mat2pmatmul  23093  decpmatmullem  23133  decpmatmul  23134  pmatcollpw1lem2  23137  pmatcollpw  23143  pmatcollpw3lem  23145  pmatcollpwscmat  23153  idpm2idmp  23163  mp2pm2mplem3  23170  mp2pm2mplem4  23171  mp2pm2mplem5  23172  mp2pm2mp  23173  pm2mpghm  23178  pm2mpmhmlem2  23181  monmat2matmon  23186  pm2mp  23187  chpdmat  23203  chpscmat  23204  chpscmatgsumbin  23206  chpscmatgsummon  23207  chp0mat  23208  chpidmat  23209  chfacfscmulgsum  23222  chfacfpmmulgsum  23226  chfacfpmmulgsum2  23227  cayhamlem1  23228  cpmidgsumm2pm  23231  cpmidpmat  23235  cpmadugsumlemB  23236  cpmadugsumlemC  23237  cpmadugsumlemF  23238  cpmadumatpoly  23245  cayhamlem3  23249  cayhamlem4  23250  cayleyhamilton0  23251  cayleyhamiltonALT  23253  neiptopnei  23494  neiptopreu  23495  ptcnplem  23984  cnmpt1t  24028  cnmpt12  24030  cnmptkp  24043  cnmptk1  24044  cnmpt1k  24045  cnmptkk  24046  cnmptk1p  24048  cnmpt2k  24051  qtopeu  24079  pt1hmeo  24169  ptunhmeo  24171  xkocnv  24177  xkohmeo  24178  flfcnp2  24370  cnmpt1plusg  24450  istgp2  24454  tmdmulg  24455  tgpmulg  24456  tmdgsum  24458  subgtgp  24468  symgtgp  24469  tgpconncomp  24476  prdstgpd  24488  tsmsmhm  24509  tsmsadd  24510  tsmssub  24512  tgptsmscls  24513  tsmssplit  24515  tsmsxplem1  24516  tsmsxplem2  24517  cnmpt1vsca  24557  tlmtgp  24559  ustuqtoplem  24602  utopsnneip  24611  ressprdsds  24734  metuval  24912  nmfval0  24953  tngnm  25014  nmoeq0  25099  idnghm  25106  cnmpt1ds  25206  fsumcn  25235  expcn  25237  divccn  25238  divccncf  25271  negcncf  25287  copco  25383  pcopt  25387  pcopt2  25388  pcoass  25389  pi1xfrcnvlem  25421  cnmpt1ip  25612  rrxnm  25756  rrxds  25758  minveclem3b  25793  divcncf  25812  ovolctb  25855  ovoliunnul  25872  voliunlem3  25917  ovolfs2  25936  uniioombllem2  25948  vitalilem4  25976  vitalilem5  25977  ismbf  25993  mbfss  26011  mbfmulc2re  26013  mbfneg  26015  mbfpos  26016  mbfposb  26018  mbfadd  26026  mbfsub  26027  mbfmulc2  26028  mbfinf  26030  mbflimsup  26031  mbflimlem  26032  i1fpos  26071  i1fposd  26072  itg1climres  26079  mbfmul  26091  itg2mulc  26112  itg2i1fseq  26120  itg2cnlem1  26126  itg2cnlem2  26127  itgresr  26143  iblneg  26167  i1fibl  26172  itgitg1  26173  iblsub  26186  itgfsum  26191  itgmulc2lem1  26196  limcmpt  26247  limccnp  26255  limcco  26257  dvreslem  26273  dvres2lem  26274  dvidlem  26279  dvcnp2  26284  dvaddbr  26302  dvmulbr  26303  dvmulf  26307  dvcmulf  26309  dvcobr  26310  dvcof  26312  dvcjbr  26313  dvcj  26314  dvfre  26315  dvexp  26317  dvexp2  26318  dvrec  26319  dvmptcmul  26328  dvmptdivc  26329  dvmptneg  26330  dvmptsub  26331  dvmptre  26333  dvmptim  26334  dvrecg  26337  dvmptdiv  26338  dvmptfsum  26339  dvcnvlem  26340  dvcnv  26341  dvexp3  26342  dvef  26344  dvsincos  26345  dv11cn  26365  lhop2  26379  lhop  26380  ftc2  26408  itgparts  26411  itgsubstlem  26412  mdegfval  26424  mdegmullem  26440  ply1termlem  26565  plypow  26567  plyconst  26568  plyeq0lem  26573  plypf1  26575  plyaddlem1  26576  plymullem1  26577  coeeulem  26587  coeidlem  26600  plyco  26604  coeeq2  26605  0dgr  26608  0dgrb  26609  dgrcolem1  26636  dgrcolem2  26637  plycjlem  26639  plymul02  26645  plyn0mulidp  26646  plymulidp  26647  dvply1  26649  dvply2g  26650  plydiveu  26663  plyremlem  26669  elqaalem3  26690  taylfval  26732  dvtaylp  26743  taylthlem1  26746  taylthlem2  26747  ulmshft  26763  mtestbdd  26778  iblulm  26780  itgulm2  26782  pserulm  26795  psercn2  26796  pserdvlem2  26801  pserdv  26802  pserdv2  26803  abelthlem1  26804  abelthlem3  26806  advlog  27028  advlogexp  27029  dvcxp1  27114  dvcxp2  27115  dvcncxp1  27117  sqrtcn  27124  loglesqrt  27135  dvatan  27309  atantayl2  27312  atantayl3  27313  leibpi  27316  rlimcnp2  27340  efrlim  27343  dfef2  27344  cxp2lim  27350  divsqrtsumlem  27353  lgamgulmlem2  27403  lgamgulm2  27409  lgamcvglem  27413  gamcvg2lem  27432  ftalem7  27452  basellem9  27462  muinv  27566  logfacrlim  27597  logexprlim  27598  dchrmullid  27625  dchrinvcl  27626  lgseisenlem3  27750  lgseisenlem4  27751  chtppilimlem2  27847  chebbnd2  27850  chpchtlim  27852  chpo1ub  27853  rpvmasumlem  27860  dchrmusumlema  27866  dchrvmasumlem1  27868  dchrvmasumiflem2  27875  dchrisum0fno1  27884  rpvmasum2  27885  dchrisum0lema  27887  dchrisum0lem1  27889  dchrisum0lem2a  27890  dchrisum0lem2  27891  dchrisum0  27893  dchrmusumlem  27895  dchrvmasumlem  27896  rpvmasum  27899  rplogsum  27900  logdivsum  27906  mulog2sumlem3  27909  vmalogdivsum2  27911  vmalogdivsum  27912  2vmadivsumlem  27913  logsqvma2  27916  log2sumbnd  27917  selberglem2  27919  selberg3lem1  27930  selberg3  27932  selberg4lem1  27933  selberg4  27934  pntrsumo1  27938  selberg3r  27942  selberg4r  27943  selberg34r  27944  pntrlog2bndlem2  27951  pntrlog2bndlem4  27953  pntrlog2bndlem5  27954  pntrlog2bndlem6  27956  padicabvf  28004  padicabvcxp  28005  mirval  29173  crctcshlem4  30455  clwlknf1oclwwlkn  30721  eucrct2eupth  30892  chscllem4  32288  brafnmul  32599  kbmul  32603  cofmpt2  33316  ofresid  33324  ofoprabco  33346  fmptunsnop  33380  fcobijfs  33399  fcobijfs2  33400  gsummpt2d  33699  gsummptres  33702  gsummptres2  33703  gsummptf1od  33705  gsummptp1  33707  gsummptfsf1o  33710  gsumfs2d  33711  gsumpart  33713  gsumhashmul  33717  gsummulsubdishift1  33718  gsummulsubdishift2  33719  gsumwrd2dccat  33728  fzto1st1  33752  fzto1st  33753  elrgspnlem1  33892  elrgspnlem2  33893  elrgspnlem3  33894  elrgspnlem4  33895  elrgspnsubrunlem1  33897  elrgspnsubrunlem2  33898  qusbas2  34054  qusima  34056  elrspunidl  34075  elrspunsn  34076  rprmdvdsprod  34163  ressply1evls1  34193  evl1deg1  34204  evl1deg2  34205  evl1deg3  34206  gsummoncoe1fzo  34225  mplasclco  34252  selvply1rhmlemb  34255  selvply1rhmlem2  34257  selvply1rhmlem4  34259  selvply1rhm0  34262  mplmulmvr  34275  evlextv  34278  mplvrpmga  34281  mplvrpmmhm  34282  mplvrpmrhm  34283  psrgsum  34284  psrmonmul  34286  issply  34297  esplyfval0  34300  esplyfval3  34308  esplyfval1  34309  esplyfvaln  34310  esplyind  34311  vietalem  34315  lbsdiflsp0  34362  fedgmullem1  34365  fedgmullem2  34366  fldextrspunlsplem  34409  fldextrspunlsp  34410  extdgfialglem2  34429  mdetpmtr1  34559  mdetlap  34568  xrge0mulc1cn  34677  esumval  34782  esumsnf  34800  esumpcvgval  34814  esumcvg  34822  esumcvgsum  34824  esumsup  34825  ofcfeqd2  34837  meascnbl  34956  sitgval  35068  probmeasb  35166  cndprobprob  35174  dstfrvclim1  35214  ballotlemfval  35226  ballotlemsval  35245  ballotlemieq  35253  signsplypnf  35283  signstfv  35296  signstfvn  35302  signstfvp  35304  itgexpif  35339  logdivsqrle  35383  ptpconn  36199  cvmliftlem6  36256  cvmliftphtlem  36283  cvmlift3lem5  36289  elmrsubrn  36486  msubfval  36490  msubco  36497  divcnvlin  36706  knoppcnlem9  37575  knoppcnlem10  37576  knoppcnlem11  37577  bj-finsumval0  38467  poimirlem3  38802  poimirlem15  38814  poimirlem16  38815  poimirlem17  38816  poimirlem19  38818  poimirlem20  38819  broucube  38833  ovoliunnfl  38841  voliunnfl  38843  volsupnfl  38844  mbfposadd  38846  itg2addnclem  38850  itg2addnclem3  38852  itg2addnc  38853  itgaddnclem2  38858  itgaddnc  38859  iblsubnc  38860  itgsubnc  38861  itgmulc2nclem1  38865  itgmulc2nclem2  38866  itgmulc2nc  38867  itgabsnc  38868  ftc1cnnclem  38870  ftc1anclem3  38874  ftc1anclem5  38876  ftc1anclem6  38877  ftc1anclem8  38879  ftc1anc  38880  ftc2nc  38881  areacirclem1  38887  areacirclem2  38888  areacirclem4  38890  areacirc  38892  upixp  38924  lcmineqlem8  43345  lcmineqlem12  43349  dvrelog2b  43375  dvrelogpow2b  43377  aks4d1p1p6  43382  aks4d1p1p5  43384  aks6d1c1  43425  aks6d1c5lem3  43446  sticksstones12a  43466  sticksstones12  43467  sticksstones19  43474  aks6d1c6lem1  43479  aks6d1c6lem4  43482  aks6d1c7lem3  43491  qsalrel  43552  rhmcomulpsr  43870  evlselv  43877  fsuppssindlem1  43879  fsuppssind  43881  mhphf  43885  mzpsubst  44019  mzprename  44020  mzpcompact2lem  44022  eldioph2  44033  rabdiophlem2  44069  mendlmod  44446  mendassa  44447  areaquad  44473  fsovcnvlem  45268  hashnzfzclim  45561  expgrowthi  45572  expgrowth  45574  uzmptshftfval  45585  dvradcnv2  45586  binomcxplemrat  45589  binomcxplemfrat  45590  binomcxplemradcnv  45591  binomcxplemdvbinom  45592  binomcxplemcvg  45593  binomcxplemdvsum  45594  binomcxplemnotnn0  45595  mulc1cncfg  46868  expcnfg  46870  fprodcnlem  46878  clim1fr1  46880  divcnvg  46906  sublimc  46929  reclimc  46930  divlimc  46933  limsupresico  46977  limsuppnfdlem  46978  limsupvaluz  46985  supcnvlimsupmpt  47018  liminfresico  47048  climliminflimsupd  47078  cncfmptssg  47148  negcncfg  47158  cncficcgt0  47165  fprodcncf  47177  fprodsubrecnncnvlem  47184  fprodaddrecnncnvlem  47186  dvsinax  47190  dvasinbx  47197  dvdivf  47199  ioodvbdlimc1lem2  47209  ioodvbdlimc2lem  47211  dvnmptdivc  47215  dvxpaek  47217  dvnxpaek  47219  dvnmul  47220  dvnprodlem2  47224  ibliccsinexp  47228  itgsinexplem1  47231  itgsinexp  47232  iblempty  47242  itgcoscmulx  47246  itgsincmulx  47251  itgioocnicc  47254  iblcncfioo  47255  itgsbtaddcnst  47259  volioofmpt  47271  volicofmpt  47274  stoweidlem4  47281  stirlinglem5  47355  dirkerval  47368  dirkertrigeq  47378  dirkeritg  47379  dirkercncflem2  47381  dirkercncflem4  47383  fourierdlem16  47400  fourierdlem18  47402  fourierdlem21  47405  fourierdlem22  47406  fourierdlem28  47412  fourierdlem39  47423  fourierdlem40  47424  fourierdlem41  47425  fourierdlem53  47436  fourierdlem56  47439  fourierdlem57  47440  fourierdlem60  47443  fourierdlem61  47444  fourierdlem68  47451  fourierdlem73  47456  fourierdlem74  47457  fourierdlem75  47458  fourierdlem76  47459  fourierdlem78  47461  fourierdlem81  47464  fourierdlem82  47465  fourierdlem83  47466  fourierdlem84  47467  fourierdlem85  47468  fourierdlem88  47471  fourierdlem90  47473  fourierdlem92  47475  fourierdlem93  47476  fourierdlem95  47478  fourierdlem97  47480  fourierdlem101  47484  fourierdlem103  47486  fourierdlem104  47487  fourierdlem111  47494  fourierdlem112  47495  sqwvfoura  47505  sqwvfourb  47506  fouriersw  47508  elaa2lem  47510  etransclem4  47515  etransclem17  47528  etransclem18  47529  etransclem32  47543  etransclem46  47557  sge0z  47652  sge0revalmpt  47655  sge0tsms  47657  sge0sup  47668  sge0iunmptlemre  47692  sge0iun  47696  sge0xaddlem2  47711  ismeannd  47744  psmeasurelem  47747  meaiuninclem  47757  meaiininclem  47763  caratheodory  47805  isomenndlem  47807  ovnval  47818  hoicvrrex  47833  ovnlecvr  47835  ovncvrrp  47841  ovn0lem  47842  ovnsubaddlem1  47847  hoidmv1lelem2  47869  hoidmv1le  47871  hoidmvlelem3  47874  ovnhoilem2  47879  ovnhoi  47880  ovnlecvr2  47887  ovncvr2  47888  hspmbllem2  47904  ovolval2lem  47920  ovolval3  47924  ovolval5lem1  47929  ovolval5lem2  47930  ovnovollem1  47933  ovnovollem2  47934  vonioolem1  47957  vonicclem1  47960  vonct  47970  smflim  48054  smfinflem  48094  smflimsuplem5  48101  smfliminflem  48107  cfsetsnfsetfv  48394  fundcmpsurbijinjpreimafv  48756  fundcmpsurinjimaid  48760  fdmdifeqresdif  49779  ply1mulgsumlem2  49824  lincvalsc0  49858  linc0scn0  49860  lincdifsn  49861  lincsum  49866  lincscm  49867  lindslinindimp2lem4  49898  lindslinindsimp2lem5  49899  lincresunit3lem2  49917  1arymaptfo  50080  itcovalpclem1  50107  itcovalpclem2  50108  itcovalt2lem1  50112  itcovalt2lem2  50113  tposcurf1  50746  tposcurf2  50747  diag1  50751  fuco22  50786  fucocolem2  50801  fucocolem3  50802  fucocolem4  50803  fucoco  50804  fucolid  50808  fucorid  50809  postcofval  50821  precofval  50827  precofvalALT  50828  precofval2  50829  fucoppcco  50869  termcpostfix  50997  islmd  51173  iscmd  51174  aacllem  51361  veronesematrowd  51403  veronesematrowexpd  51404  veroquadmodzerod  51406  amgmwlem  51409