Theorem mpteq2dva 5242

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

Syntax hints:   → wi 4   ∧ wa 396   = wceq 1541   ∈ wcel 2106   ↦ cmpt 5225

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2703

This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1782  df-sb 2068  df-clab 2710  df-cleq 2724  df-clel 2810  df-opab 5205  df-mpt 5226

This theorem is referenced by:  mpteq2dv  5244  mpteq2ia  5245  2fvcoidd  7280  offval  7663  offval2  7674  caofinvl  7684  caofcom  7689  caofass  7691  caofdi  7693  caofdir  7694  caonncan  7695  curry1  8074  curry2  8077  mpocurryd  8238  pw2f1olem  9061  mapxpen  9128  xpmapenlem  9129  cantnfp1  9660  cantnflem1d  9667  cantnflem1  9668  cnfcom2lem  9680  dfac12lem1  10122  seqof  14009  seqof2  14010  swrdswrd  14639  repswswrd  14718  repswrevw  14721  revco  14769  ccatco  14770  repsco  14775  ofccat  14900  lo1eq  15496  rlimeq  15497  lo1mul2  15557  o1dif  15558  lo1sub  15559  rlimdiv  15576  caucvgr  15606  sumeq1  15619  fsumrlim  15741  fsumo1  15742  climfsum  15750  geomulcvg  15806  vdwlem8  16905  prmgapprmo  16979  restid2  17360  pwsplusgval  17420  pwsmulrval  17421  pwsvscafval  17424  qusin  17474  xpsaddlem  17503  xpsvsca  17507  catidd  17608  fuclid  17903  fucrid  17904  fucass  17905  setcepi  18022  prf1st  18140  prf2nd  18141  1st2ndprf  18142  curfcl  18169  curfuncf  18175  diag2  18182  curf2ndf  18184  hof2val  18193  hofcllem  18195  hofcl  18196  yonedalem4a  18212  yonedalem4c  18214  yonedalem3b  18216  yonedainv  18218  yonffthlem  18219  prdsidlem  18636  prdsmndd  18637  pwsco2mhm  18691  frmdup3lem  18724  frmdup3  18725  smndex1gid  18761  smndex1igid  18762  grpinvpropd  18874  prdsinvlem  18908  pwsinvg  18912  pwssub  18913  galactghm  19238  cayleylem1  19246  pmtrprfval  19321  sylow1lem2  19433  sylow3lem1  19461  efginvrel1  19562  frgpup3lem  19611  frgpup3  19612  prdscmnd  19691  iscyggen  19709  gsumval3  19736  gsumcllem  19737  gsumzsplit  19756  gsumsub  19777  gsummptf1o  19792  gsum2d  19801  gsum2d2  19803  gsumxp  19805  prdsgsum  19810  telgsumfz  19819  telgsumfz0  19821  telgsum  19823  dprdfsub  19852  dprdfeq0  19853  dprddisj2  19870  dprd2d2  19875  dpjidcl  19889  ablfaclem2  19917  ablfac2  19920  srgbinomlem3  20011  srgbinomlem4  20012  srgbinomlem  20013  gsumdixp  20088  prdsmgp  20089  prdsringd  20091  prdslmodd  20531  mulgrhm2  20983  frgpcyg  21064  evpmodpmf1o  21084  phlpropd  21143  frlmphl  21271  uvcresum  21283  frlmup1  21288  asclpropd  21384  psrass1lemOLD  21426  psrass1lem  21429  psrlinv  21449  psrass1  21458  psrdi  21459  psrdir  21460  psrass23l  21461  psrcom  21462  psrass23  21463  resspsrmul  21470  mplsubrglem  21494  mplmonmul  21521  mplcoe1  21522  mplcoe5  21525  mplcoe4  21563  evlslem3  21574  evlslem1  21576  mhpmulcl  21623  psrplusgpropd  21691  psropprmul  21693  coe1mul2  21724  coe1tm  21728  coe1tmmul2  21731  coe1tmmul  21732  coe1pwmul  21734  cply1mul  21749  ply1coe  21751  eqcoe1ply1eq  21752  lply1binomsc  21762  evl1gsummon  21815  mamures  21823  grpvrinv  21829  mhmvlin  21830  mamuass  21833  mamudi  21834  mamudir  21835  mamuvs1  21836  mamuvs2  21837  mpomatmul  21879  mamutpos  21891  madetsumid  21894  dmatmul  21930  scmatscm  21946  1mavmul  21981  mavmulass  21982  mvmumamul1  21987  mulmarep1gsum1  22006  mulmarep1gsum2  22007  mdetleib2  22021  mdetfval1  22023  mdet0pr  22025  mdetdiag  22032  mdetdiagid  22033  mdetrlin  22035  mdetrsca  22036  mdetralt  22041  mdetunilem9  22053  gsummatr01  22092  smadiadetlem1a  22096  smadiadetlem3  22101  smadiadetlem4  22102  cpmatmcllem  22151  mat2pmatmul  22164  decpmatmullem  22204  decpmatmul  22205  pmatcollpw1lem2  22208  pmatcollpw  22214  pmatcollpw3lem  22216  pmatcollpwscmat  22224  idpm2idmp  22234  mp2pm2mplem3  22241  mp2pm2mplem4  22242  mp2pm2mplem5  22243  mp2pm2mp  22244  pm2mpghm  22249  pm2mpmhmlem2  22252  monmat2matmon  22257  pm2mp  22258  chpdmat  22274  chpscmat  22275  chpscmatgsumbin  22277  chpscmatgsummon  22278  chp0mat  22279  chpidmat  22280  chfacfscmulgsum  22293  chfacfpmmulgsum  22297  chfacfpmmulgsum2  22298  cayhamlem1  22299  cpmidgsumm2pm  22302  cpmidpmat  22306  cpmadugsumlemB  22307  cpmadugsumlemC  22308  cpmadugsumlemF  22309  cpmadumatpoly  22316  cayhamlem3  22320  cayhamlem4  22321  cayleyhamilton0  22322  cayleyhamiltonALT  22324  neiptopnei  22567  neiptopreu  22568  ptcnplem  23056  cnmpt1t  23100  cnmpt12  23102  cnmptkp  23115  cnmptk1  23116  cnmpt1k  23117  cnmptkk  23118  cnmptk1p  23120  cnmpt2k  23123  qtopeu  23151  pt1hmeo  23241  ptunhmeo  23243  xkocnv  23249  xkohmeo  23250  flfcnp2  23442  cnmpt1plusg  23522  istgp2  23526  tmdmulg  23527  tgpmulg  23528  tmdgsum  23530  subgtgp  23540  symgtgp  23541  tgpconncomp  23548  prdstgpd  23560  tsmsmhm  23581  tsmsadd  23582  tsmssub  23584  tgptsmscls  23585  tsmssplit  23587  tsmsxplem1  23588  tsmsxplem2  23589  cnmpt1vsca  23629  tlmtgp  23631  ustuqtoplem  23675  utopsnneip  23684  ressprdsds  23808  metuval  23989  nmfval0  24030  tngnm  24099  nmoeq0  24184  idnghm  24191  cnmpt1ds  24289  fsumcn  24317  expcn  24319  divccn  24320  divccncf  24353  negcncf  24369  copco  24465  pcopt  24469  pcopt2  24470  pcoass  24471  pi1xfrcnvlem  24503  cnmpt1ip  24695  rrxnm  24839  rrxds  24841  minveclem3b  24876  divcncf  24895  ovolctb  24938  ovoliunnul  24955  voliunlem3  25000  ovolfs2  25019  uniioombllem2  25031  vitalilem4  25059  vitalilem5  25060  ismbf  25076  mbfss  25094  mbfmulc2re  25096  mbfneg  25098  mbfpos  25099  mbfposb  25101  mbfadd  25109  mbfsub  25110  mbfmulc2  25111  mbfinf  25113  mbflimsup  25114  mbflimlem  25115  i1fpos  25155  i1fposd  25156  itg1climres  25163  mbfmul  25175  itg2mulc  25196  itg2i1fseq  25204  itg2cnlem1  25210  itg2cnlem2  25211  itgresr  25227  iblneg  25251  i1fibl  25256  itgitg1  25257  iblsub  25270  itgfsum  25275  itgmulc2lem1  25280  limcmpt  25331  limccnp  25339  limcco  25341  dvreslem  25357  dvres2lem  25358  dvidlem  25363  dvcnp2  25368  dvaddbr  25386  dvmulbr  25387  dvmulf  25391  dvcmulf  25393  dvcobr  25394  dvcof  25396  dvcjbr  25397  dvcj  25398  dvfre  25399  dvexp  25401  dvexp2  25402  dvrec  25403  dvmptcmul  25412  dvmptdivc  25413  dvmptneg  25414  dvmptsub  25415  dvmptre  25417  dvmptim  25418  dvrecg  25421  dvmptdiv  25422  dvmptfsum  25423  dvcnvlem  25424  dvcnv  25425  dvexp3  25426  dvef  25428  dvsincos  25429  dv11cn  25449  lhop2  25463  lhop  25464  ftc2  25492  itgparts  25495  itgsubstlem  25496  mdegfval  25511  mdegmullem  25527  ply1termlem  25648  plypow  25650  plyconst  25651  plyeq0lem  25655  plypf1  25657  plyaddlem1  25658  plymullem1  25659  coeeulem  25669  coeidlem  25682  plyco  25686  coeeq2  25687  0dgr  25690  0dgrb  25691  dgrcolem1  25718  dgrcolem2  25719  plycjlem  25721  dvply1  25728  dvply2g  25729  plydiveu  25742  plyremlem  25748  elqaalem3  25765  taylfval  25802  dvtaylp  25813  taylthlem1  25816  taylthlem2  25817  ulmshft  25833  mtestbdd  25848  iblulm  25850  itgulm2  25852  pserulm  25865  psercn2  25866  pserdvlem2  25871  pserdv  25872  pserdv2  25873  abelthlem1  25874  abelthlem3  25876  advlog  26093  advlogexp  26094  dvcxp1  26177  dvcxp2  26178  dvcncxp1  26180  sqrtcn  26187  loglesqrt  26195  dvatan  26369  atantayl2  26372  atantayl3  26373  leibpi  26376  rlimcnp2  26400  efrlim  26403  dfef2  26404  cxp2lim  26410  divsqrtsumlem  26413  lgamgulmlem2  26463  lgamgulm2  26469  lgamcvglem  26473  gamcvg2lem  26492  ftalem7  26512  basellem9  26522  muinv  26626  logfacrlim  26656  logexprlim  26657  dchrmullid  26684  dchrinvcl  26685  lgseisenlem3  26809  lgseisenlem4  26810  chtppilimlem2  26906  chebbnd2  26909  chpchtlim  26911  chpo1ub  26912  rpvmasumlem  26919  dchrmusumlema  26925  dchrvmasumlem1  26927  dchrvmasumiflem2  26934  dchrisum0fno1  26943  rpvmasum2  26944  dchrisum0lema  26946  dchrisum0lem1  26948  dchrisum0lem2a  26949  dchrisum0lem2  26950  dchrisum0  26952  dchrmusumlem  26954  dchrvmasumlem  26955  rpvmasum  26958  rplogsum  26959  logdivsum  26965  mulog2sumlem3  26968  vmalogdivsum2  26970  vmalogdivsum  26971  2vmadivsumlem  26972  logsqvma2  26975  log2sumbnd  26976  selberglem2  26978  selberg3lem1  26989  selberg3  26991  selberg4lem1  26992  selberg4  26993  pntrsumo1  26997  selberg3r  27001  selberg4r  27002  selberg34r  27003  pntrlog2bndlem2  27010  pntrlog2bndlem4  27012  pntrlog2bndlem5  27013  pntrlog2bndlem6  27015  padicabvf  27063  padicabvcxp  27064  mirval  27835  crctcshlem4  29003  clwlknf1oclwwlkn  29266  eucrct2eupth  29427  chscllem4  30820  brafnmul  31131  kbmul  31135  cofmpt2  31790  ofresid  31800  ofoprabco  31822  fcobijfs  31883  gsummpt2d  32136  gsummptres  32139  gsummptres2  32140  gsumpart  32142  gsumhashmul  32143  fzto1st1  32196  fzto1st  32197  freshmansdream  32313  qusima  32440  elrspunidl  32461  elrspunsn  32462  evls1fpws  32553  gsummoncoe1fzo  32572  lbsdiflsp0  32613  fedgmullem1  32616  fedgmullem2  32617  mdetpmtr1  32698  mdetlap  32707  xrge0mulc1cn  32816  esumval  32939  esumsnf  32957  esumpcvgval  32971  esumcvg  32979  esumcvgsum  32981  esumsup  32982  ofcfeqd2  32994  meascnbl  33112  sitgval  33226  probmeasb  33324  cndprobprob  33332  dstfrvclim1  33371  ballotlemfval  33383  ballotlemsval  33402  ballotlemieq  33410  plymul02  33452  plymulx0  33453  plymulx  33454  signsplypnf  33456  signstfv  33469  signstfvn  33475  signstfvp  33477  itgexpif  33513  logdivsqrle  33557  ptpconn  34119  cvmliftlem6  34176  cvmliftphtlem  34203  cvmlift3lem5  34209  elmrsubrn  34406  msubfval  34410  msubco  34417  divcnvlin  34596  knoppcnlem9  35245  knoppcnlem10  35246  knoppcnlem11  35247  bj-finsumval0  36034  curf  36334  matunitlindflem1  36352  matunitlindflem2  36353  poimirlem3  36359  poimirlem15  36371  poimirlem16  36372  poimirlem17  36373  poimirlem19  36375  poimirlem20  36376  broucube  36390  ovoliunnfl  36398  voliunnfl  36400  volsupnfl  36401  mbfposadd  36403  itg2addnclem  36407  itg2addnclem3  36409  itg2addnc  36410  itgaddnclem2  36415  itgaddnc  36416  iblsubnc  36417  itgsubnc  36418  itgmulc2nclem1  36422  itgmulc2nclem2  36423  itgmulc2nc  36424  itgabsnc  36425  ftc1cnnclem  36427  ftc1anclem3  36431  ftc1anclem5  36433  ftc1anclem6  36434  ftc1anclem8  36436  ftc1anc  36437  ftc2nc  36438  areacirclem1  36444  areacirclem2  36445  areacirclem4  36447  areacirc  36449  upixp  36466  lcmineqlem8  40770  lcmineqlem12  40774  dvrelog2b  40800  dvrelogpow2b  40802  aks4d1p1p6  40807  aks4d1p1p5  40809  sticksstones12a  40842  sticksstones12  40843  sticksstones19  40850  qsalrel  40938  pwsgprod  40982  rhmcomulmpl  40990  evlsbagval  40998  evlsevl  41002  fsuppssindlem1  41016  fsuppssind  41018  mhphf  41021  mzpsubst  41321  mzprename  41322  mzpcompact2lem  41324  eldioph2  41335  rabdiophlem2  41375  mendlmod  41770  mendassa  41771  areaquad  41800  fsovcnvlem  42599  hashnzfzclim  42916  expgrowthi  42927  expgrowth  42929  uzmptshftfval  42940  dvradcnv2  42941  binomcxplemrat  42944  binomcxplemfrat  42945  binomcxplemradcnv  42946  binomcxplemdvbinom  42947  binomcxplemcvg  42948  binomcxplemdvsum  42949  binomcxplemnotnn0  42950  mulc1cncfg  44142  expcnfg  44144  fprodcnlem  44152  clim1fr1  44154  divcnvg  44180  sublimc  44205  reclimc  44206  divlimc  44209  limsupresico  44253  limsuppnfdlem  44254  limsupvaluz  44261  supcnvlimsupmpt  44294  liminfresico  44324  climliminflimsupd  44354  cncfmptssg  44424  negcncfg  44434  cncficcgt0  44441  fprodcncf  44453  fprodsubrecnncnvlem  44460  fprodaddrecnncnvlem  44462  dvsinax  44466  dvasinbx  44473  dvdivf  44475  ioodvbdlimc1lem2  44485  ioodvbdlimc2lem  44487  dvnmptdivc  44491  dvxpaek  44493  dvnxpaek  44495  dvnmul  44496  dvnprodlem2  44500  ibliccsinexp  44504  itgsinexplem1  44507  itgsinexp  44508  iblempty  44518  itgcoscmulx  44522  itgsincmulx  44527  itgioocnicc  44530  iblcncfioo  44531  itgsbtaddcnst  44535  volioofmpt  44547  volicofmpt  44550  stoweidlem4  44557  stirlinglem5  44631  dirkerval  44644  dirkertrigeq  44654  dirkeritg  44655  dirkercncflem2  44657  dirkercncflem4  44659  fourierdlem16  44676  fourierdlem18  44678  fourierdlem21  44681  fourierdlem22  44682  fourierdlem28  44688  fourierdlem39  44699  fourierdlem40  44700  fourierdlem41  44701  fourierdlem53  44712  fourierdlem56  44715  fourierdlem57  44716  fourierdlem60  44719  fourierdlem61  44720  fourierdlem68  44727  fourierdlem73  44732  fourierdlem74  44733  fourierdlem75  44734  fourierdlem76  44735  fourierdlem78  44737  fourierdlem81  44740  fourierdlem82  44741  fourierdlem83  44742  fourierdlem84  44743  fourierdlem85  44744  fourierdlem88  44747  fourierdlem90  44749  fourierdlem92  44751  fourierdlem93  44752  fourierdlem95  44754  fourierdlem97  44756  fourierdlem101  44760  fourierdlem103  44762  fourierdlem104  44763  fourierdlem111  44770  fourierdlem112  44771  sqwvfoura  44781  sqwvfourb  44782  fouriersw  44784  elaa2lem  44786  etransclem4  44791  etransclem17  44804  etransclem18  44805  etransclem32  44819  etransclem46  44833  sge0z  44928  sge0revalmpt  44931  sge0tsms  44933  sge0sup  44944  sge0iunmptlemre  44968  sge0iun  44972  sge0xaddlem2  44987  ismeannd  45020  psmeasurelem  45023  meaiuninclem  45033  meaiininclem  45039  caratheodory  45081  isomenndlem  45083  ovnval  45094  hoicvrrex  45109  ovnlecvr  45111  ovncvrrp  45117  ovn0lem  45118  ovnsubaddlem1  45123  hoidmv1lelem2  45145  hoidmv1le  45147  hoidmvlelem3  45150  ovnhoilem2  45155  ovnhoi  45156  ovnlecvr2  45163  ovncvr2  45164  hspmbllem2  45180  ovolval2lem  45196  ovolval3  45200  ovolval5lem1  45205  ovolval5lem2  45206  ovnovollem1  45209  ovnovollem2  45210  vonioolem1  45233  vonicclem1  45236  vonct  45246  smflim  45330  smfinflem  45370  smflimsuplem5  45377  smfliminflem  45383  cfsetsnfsetfv  45603  fundcmpsurbijinjpreimafv  45911  fundcmpsurinjimaid  45915  fdmdifeqresdif  46729  ply1mulgsumlem2  46780  lincvalsc0  46814  linc0scn0  46816  lincdifsn  46817  lincsum  46822  lincscm  46823  lindslinindimp2lem4  46854  lindslinindsimp2lem5  46855  lincresunit3lem2  46873  1arymaptfo  47041  itcovalpclem1  47068  itcovalpclem2  47069  itcovalt2lem1  47073  itcovalt2lem2  47074  aacllem  47560  amgmwlem  47561