Theorem mpteq2dva 5193

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

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1542   ∈ wcel 2114   ↦ cmpt 5181

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 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-opab 5163  df-mpt 5182

This theorem is referenced by:  mpteq2dv  5194  mpteq2ia  5195  2fvcoidd  7253  offval  7641  offval2  7652  coof  7656  caofinvl  7664  caofcom  7669  caofass  7672  caofdi  7674  caofdir  7675  caonncan  7676  curry1  8056  curry2  8059  mpocurryd  8221  pw2f1olem  9021  mapxpen  9083  xpmapenlem  9084  cantnfp1  9602  cantnflem1d  9609  cantnflem1  9610  cnfcom2lem  9622  dfac12lem1  10066  seqof  13994  seqof2  13995  swrdswrd  14640  repswswrd  14719  repswrevw  14722  revco  14769  ccatco  14770  repsco  14775  ofccat  14904  lo1eq  15503  rlimeq  15504  lo1mul2  15564  o1dif  15565  lo1sub  15566  rlimdiv  15581  caucvgr  15611  sumeq1  15624  fsumrlim  15746  fsumo1  15747  climfsum  15755  geomulcvg  15811  vdwlem8  16928  prmgapprmo  17002  restid2  17362  pwsplusgval  17423  pwsmulrval  17424  pwsvscafval  17427  qusin  17477  xpsaddlem  17506  xpsvsca  17510  catidd  17615  fuclid  17905  fucrid  17906  fucass  17907  setcepi  18024  prf1st  18139  prf2nd  18140  1st2ndprf  18141  curfcl  18167  curfuncf  18173  diag2  18180  curf2ndf  18182  hof2val  18191  hofcllem  18193  hofcl  18194  yonedalem4a  18210  yonedalem4c  18212  yonedalem3b  18214  yonedainv  18216  yonffthlem  18217  prdssgrpd  18670  prdsidlem  18706  prdsmndd  18707  mhmvlin  18738  pwsco2mhm  18770  frmdup3lem  18803  frmdup3  18804  smndex1gid  18840  smndex1igid  18841  grpinvpropd  18957  prdsinvlem  18991  pwsinvg  18995  pwssub  18996  galactghm  19345  cayleylem1  19353  pmtrprfval  19428  sylow1lem2  19540  sylow3lem1  19568  efginvrel1  19669  frgpup3lem  19718  frgpup3  19719  prdscmnd  19802  iscyggen  19821  gsumval3  19848  gsumcllem  19849  gsumzsplit  19868  gsumsub  19889  gsummptf1o  19904  gsum2d  19913  gsum2d2  19915  gsumxp  19917  prdsgsum  19922  telgsumfz  19931  telgsumfz0  19933  telgsum  19935  dprdfsub  19964  dprdfeq0  19965  dprddisj2  19982  dprd2d2  19987  dpjidcl  20001  ablfaclem2  20029  ablfac2  20032  prdsmgp  20098  prdsrngd  20123  srgbinomlem3  20175  srgbinomlem4  20176  srgbinomlem  20177  gsumdixp  20266  prdsringd  20268  pwsgprod  20277  prdslmodd  20932  mulgrhm2  21445  frgpcyg  21540  freshmansdream  21541  evpmodpmf1o  21563  phlpropd  21622  frlmphl  21748  uvcresum  21760  frlmup1  21765  asclpropd  21865  psrass1lem  21900  psrlinv  21923  psrass1  21931  psrdi  21932  psrdir  21933  psrass23l  21934  psrcom  21935  psrass23  21936  resspsrmul  21943  mplsubrglem  21971  mplmonmul  22003  mplcoe1  22004  mplcoe5  22007  mplcoe4  22038  evlslem3  22047  evlslem1  22049  evlsvvval  22060  mhpmulcl  22104  psdmplcl  22117  psdadd  22118  psdmul  22121  psdmvr  22124  psrplusgpropd  22188  psropprmul  22190  coe1mul2  22223  coe1tm  22227  coe1tmmul2  22230  coe1tmmul  22231  coe1pwmul  22233  cply1mul  22252  ply1coe  22254  eqcoe1ply1eq  22255  lply1binomsc  22267  evl1gsummon  22321  evls1fpws  22325  rhmcomulmpl  22338  mamures  22353  grpvrinv  22355  mamuass  22358  mamudi  22359  mamudir  22360  mamuvs1  22361  mamuvs2  22362  mpomatmul  22402  mamutpos  22414  madetsumid  22417  dmatmul  22453  scmatscm  22469  1mavmul  22504  mavmulass  22505  mvmumamul1  22510  mulmarep1gsum1  22529  mulmarep1gsum2  22530  mdetleib2  22544  mdetfval1  22546  mdet0pr  22548  mdetdiag  22555  mdetdiagid  22556  mdetrlin  22558  mdetrsca  22559  mdetralt  22564  mdetunilem9  22576  gsummatr01  22615  smadiadetlem1a  22619  smadiadetlem3  22624  smadiadetlem4  22625  cpmatmcllem  22674  mat2pmatmul  22687  decpmatmullem  22727  decpmatmul  22728  pmatcollpw1lem2  22731  pmatcollpw  22737  pmatcollpw3lem  22739  pmatcollpwscmat  22747  idpm2idmp  22757  mp2pm2mplem3  22764  mp2pm2mplem4  22765  mp2pm2mplem5  22766  mp2pm2mp  22767  pm2mpghm  22772  pm2mpmhmlem2  22775  monmat2matmon  22780  pm2mp  22781  chpdmat  22797  chpscmat  22798  chpscmatgsumbin  22800  chpscmatgsummon  22801  chp0mat  22802  chpidmat  22803  chfacfscmulgsum  22816  chfacfpmmulgsum  22820  chfacfpmmulgsum2  22821  cayhamlem1  22822  cpmidgsumm2pm  22825  cpmidpmat  22829  cpmadugsumlemB  22830  cpmadugsumlemC  22831  cpmadugsumlemF  22832  cpmadumatpoly  22839  cayhamlem3  22843  cayhamlem4  22844  cayleyhamilton0  22845  cayleyhamiltonALT  22847  neiptopnei  23088  neiptopreu  23089  ptcnplem  23577  cnmpt1t  23621  cnmpt12  23623  cnmptkp  23636  cnmptk1  23637  cnmpt1k  23638  cnmptkk  23639  cnmptk1p  23641  cnmpt2k  23644  qtopeu  23672  pt1hmeo  23762  ptunhmeo  23764  xkocnv  23770  xkohmeo  23771  flfcnp2  23963  cnmpt1plusg  24043  istgp2  24047  tmdmulg  24048  tgpmulg  24049  tmdgsum  24051  subgtgp  24061  symgtgp  24062  tgpconncomp  24069  prdstgpd  24081  tsmsmhm  24102  tsmsadd  24103  tsmssub  24105  tgptsmscls  24106  tsmssplit  24108  tsmsxplem1  24109  tsmsxplem2  24110  cnmpt1vsca  24150  tlmtgp  24152  ustuqtoplem  24195  utopsnneip  24204  ressprdsds  24327  metuval  24505  nmfval0  24546  tngnm  24607  nmoeq0  24692  idnghm  24699  cnmpt1ds  24799  fsumcn  24829  expcn  24831  divccn  24832  expcnOLD  24833  divccnOLD  24834  divccncf  24867  negcncf  24883  negcncfOLD  24884  copco  24986  pcopt  24990  pcopt2  24991  pcoass  24992  pi1xfrcnvlem  25024  cnmpt1ip  25215  rrxnm  25359  rrxds  25361  minveclem3b  25396  divcncf  25416  ovolctb  25459  ovoliunnul  25476  voliunlem3  25521  ovolfs2  25540  uniioombllem2  25552  vitalilem4  25580  vitalilem5  25581  ismbf  25597  mbfss  25615  mbfmulc2re  25617  mbfneg  25619  mbfpos  25620  mbfposb  25622  mbfadd  25630  mbfsub  25631  mbfmulc2  25632  mbfinf  25634  mbflimsup  25635  mbflimlem  25636  i1fpos  25675  i1fposd  25676  itg1climres  25683  mbfmul  25695  itg2mulc  25716  itg2i1fseq  25724  itg2cnlem1  25730  itg2cnlem2  25731  itgresr  25748  iblneg  25772  i1fibl  25777  itgitg1  25778  iblsub  25791  itgfsum  25796  itgmulc2lem1  25801  limcmpt  25852  limccnp  25860  limcco  25862  dvreslem  25878  dvres2lem  25879  dvidlem  25884  dvcnp2  25889  dvcnp2OLD  25890  dvaddbr  25908  dvmulbr  25909  dvmulbrOLD  25910  dvmulf  25914  dvcmulf  25916  dvcobr  25917  dvcobrOLD  25918  dvcof  25920  dvcjbr  25921  dvcj  25922  dvfre  25923  dvexp  25925  dvexp2  25926  dvrec  25927  dvmptcmul  25936  dvmptdivc  25937  dvmptneg  25938  dvmptsub  25939  dvmptre  25941  dvmptim  25942  dvrecg  25945  dvmptdiv  25946  dvmptfsum  25947  dvcnvlem  25948  dvcnv  25949  dvexp3  25950  dvef  25952  dvsincos  25953  dv11cn  25974  lhop2  25988  lhop  25989  ftc2  26019  itgparts  26022  itgsubstlem  26023  mdegfval  26035  mdegmullem  26051  ply1termlem  26176  plypow  26178  plyconst  26179  plyeq0lem  26183  plypf1  26185  plyaddlem1  26186  plymullem1  26187  coeeulem  26197  coeidlem  26210  plyco  26214  coeeq2  26215  0dgr  26218  0dgrb  26219  dgrcolem1  26247  dgrcolem2  26248  plycjlem  26250  dvply1  26259  dvply2g  26260  dvply2gOLD  26261  plydiveu  26274  plyremlem  26280  elqaalem3  26297  taylfval  26334  dvtaylp  26346  taylthlem1  26349  taylthlem2  26350  taylthlem2OLD  26351  ulmshft  26367  mtestbdd  26382  iblulm  26384  itgulm2  26386  pserulm  26399  psercn2  26400  psercn2OLD  26401  pserdvlem2  26406  pserdv  26407  pserdv2  26408  abelthlem1  26409  abelthlem3  26411  advlog  26631  advlogexp  26632  dvcxp1  26717  dvcxp2  26718  dvcncxp1  26720  sqrtcn  26728  loglesqrt  26739  dvatan  26913  atantayl2  26916  atantayl3  26917  leibpi  26920  rlimcnp2  26944  efrlim  26947  efrlimOLD  26948  dfef2  26949  cxp2lim  26955  divsqrtsumlem  26958  lgamgulmlem2  27008  lgamgulm2  27014  lgamcvglem  27018  gamcvg2lem  27037  ftalem7  27057  basellem9  27067  muinv  27171  logfacrlim  27203  logexprlim  27204  dchrmullid  27231  dchrinvcl  27232  lgseisenlem3  27356  lgseisenlem4  27357  chtppilimlem2  27453  chebbnd2  27456  chpchtlim  27458  chpo1ub  27459  rpvmasumlem  27466  dchrmusumlema  27472  dchrvmasumlem1  27474  dchrvmasumiflem2  27481  dchrisum0fno1  27490  rpvmasum2  27491  dchrisum0lema  27493  dchrisum0lem1  27495  dchrisum0lem2a  27496  dchrisum0lem2  27497  dchrisum0  27499  dchrmusumlem  27501  dchrvmasumlem  27502  rpvmasum  27505  rplogsum  27506  logdivsum  27512  mulog2sumlem3  27515  vmalogdivsum2  27517  vmalogdivsum  27518  2vmadivsumlem  27519  logsqvma2  27522  log2sumbnd  27523  selberglem2  27525  selberg3lem1  27536  selberg3  27538  selberg4lem1  27539  selberg4  27540  pntrsumo1  27544  selberg3r  27548  selberg4r  27549  selberg34r  27550  pntrlog2bndlem2  27557  pntrlog2bndlem4  27559  pntrlog2bndlem5  27560  pntrlog2bndlem6  27562  padicabvf  27610  padicabvcxp  27611  mirval  28739  crctcshlem4  29905  clwlknf1oclwwlkn  30171  eucrct2eupth  30332  chscllem4  31727  brafnmul  32038  kbmul  32042  cofmpt2  32723  ofresid  32731  ofoprabco  32753  fmptunsnop  32789  fcobijfs  32810  fcobijfs2  32811  gsummpt2d  33142  gsummptres  33145  gsummptres2  33146  gsummptf1od  33148  gsummptp1  33150  gsummptfsf1o  33153  gsumfs2d  33154  gsumpart  33156  gsumhashmul  33160  gsummulsubdishift1  33161  gsummulsubdishift2  33162  gsumwrd2dccat  33171  fzto1st1  33195  fzto1st  33196  elrgspnlem1  33335  elrgspnlem2  33336  elrgspnlem3  33337  elrgspnlem4  33338  elrgspnsubrunlem1  33340  elrgspnsubrunlem2  33341  qusbas2  33498  qusima  33500  elrspunidl  33520  elrspunsn  33521  rprmdvdsprod  33626  ressply1evls1  33657  evl1deg1  33668  evl1deg2  33669  evl1deg3  33670  gsummoncoe1fzo  33689  mplmulmvr  33715  evlextv  33718  mplvrpmga  33721  mplvrpmmhm  33722  mplvrpmrhm  33723  psrgsum  33724  psrmonmul  33726  issply  33737  esplyfval0  33740  esplyfval3  33748  esplyfval1  33749  esplyfvaln  33750  esplyind  33751  vietalem  33755  lbsdiflsp0  33803  fedgmullem1  33806  fedgmullem2  33807  fldextrspunlsplem  33850  fldextrspunlsp  33851  extdgfialglem2  33870  mdetpmtr1  34000  mdetlap  34009  xrge0mulc1cn  34118  esumval  34223  esumsnf  34241  esumpcvgval  34255  esumcvg  34263  esumcvgsum  34265  esumsup  34266  ofcfeqd2  34278  meascnbl  34396  sitgval  34509  probmeasb  34607  cndprobprob  34615  dstfrvclim1  34655  ballotlemfval  34667  ballotlemsval  34686  ballotlemieq  34694  plymul02  34723  plymulx0  34724  plymulx  34725  signsplypnf  34727  signstfv  34740  signstfvn  34746  signstfvp  34748  itgexpif  34783  logdivsqrle  34827  ptpconn  35446  cvmliftlem6  35503  cvmliftphtlem  35530  cvmlift3lem5  35536  elmrsubrn  35733  msubfval  35737  msubco  35744  divcnvlin  35946  knoppcnlem9  36720  knoppcnlem10  36721  knoppcnlem11  36722  bj-finsumval0  37537  curf  37846  matunitlindflem1  37864  matunitlindflem2  37865  poimirlem3  37871  poimirlem15  37883  poimirlem16  37884  poimirlem17  37885  poimirlem19  37887  poimirlem20  37888  broucube  37902  ovoliunnfl  37910  voliunnfl  37912  volsupnfl  37913  mbfposadd  37915  itg2addnclem  37919  itg2addnclem3  37921  itg2addnc  37922  itgaddnclem2  37927  itgaddnc  37928  iblsubnc  37929  itgsubnc  37930  itgmulc2nclem1  37934  itgmulc2nclem2  37935  itgmulc2nc  37936  itgabsnc  37937  ftc1cnnclem  37939  ftc1anclem3  37943  ftc1anclem5  37945  ftc1anclem6  37946  ftc1anclem8  37948  ftc1anc  37949  ftc2nc  37950  areacirclem1  37956  areacirclem2  37957  areacirclem4  37959  areacirc  37961  upixp  37977  lcmineqlem8  42403  lcmineqlem12  42407  dvrelog2b  42433  dvrelogpow2b  42435  aks4d1p1p6  42440  aks4d1p1p5  42442  aks6d1c1  42483  aks6d1c5lem3  42504  sticksstones12a  42524  sticksstones12  42525  sticksstones19  42532  aks6d1c6lem1  42537  aks6d1c6lem4  42540  aks6d1c7lem3  42549  qsalrel  42608  rhmcomulpsr  42916  evlsevl  42929  selvvvval  42940  evlselv  42942  fsuppssindlem1  42946  fsuppssind  42948  mhphf  42952  mzpsubst  43102  mzprename  43103  mzpcompact2lem  43105  eldioph2  43116  rabdiophlem2  43156  mendlmod  43543  mendassa  43544  areaquad  43570  fsovcnvlem  44366  hashnzfzclim  44675  expgrowthi  44686  expgrowth  44688  uzmptshftfval  44699  dvradcnv2  44700  binomcxplemrat  44703  binomcxplemfrat  44704  binomcxplemradcnv  44705  binomcxplemdvbinom  44706  binomcxplemcvg  44707  binomcxplemdvsum  44708  binomcxplemnotnn0  44709  mulc1cncfg  45946  expcnfg  45948  fprodcnlem  45956  clim1fr1  45958  divcnvg  45984  sublimc  46007  reclimc  46008  divlimc  46011  limsupresico  46055  limsuppnfdlem  46056  limsupvaluz  46063  supcnvlimsupmpt  46096  liminfresico  46126  climliminflimsupd  46156  cncfmptssg  46226  negcncfg  46236  cncficcgt0  46243  fprodcncf  46255  fprodsubrecnncnvlem  46262  fprodaddrecnncnvlem  46264  dvsinax  46268  dvasinbx  46275  dvdivf  46277  ioodvbdlimc1lem2  46287  ioodvbdlimc2lem  46289  dvnmptdivc  46293  dvxpaek  46295  dvnxpaek  46297  dvnmul  46298  dvnprodlem2  46302  ibliccsinexp  46306  itgsinexplem1  46309  itgsinexp  46310  iblempty  46320  itgcoscmulx  46324  itgsincmulx  46329  itgioocnicc  46332  iblcncfioo  46333  itgsbtaddcnst  46337  volioofmpt  46349  volicofmpt  46352  stoweidlem4  46359  stirlinglem5  46433  dirkerval  46446  dirkertrigeq  46456  dirkeritg  46457  dirkercncflem2  46459  dirkercncflem4  46461  fourierdlem16  46478  fourierdlem18  46480  fourierdlem21  46483  fourierdlem22  46484  fourierdlem28  46490  fourierdlem39  46501  fourierdlem40  46502  fourierdlem41  46503  fourierdlem53  46514  fourierdlem56  46517  fourierdlem57  46518  fourierdlem60  46521  fourierdlem61  46522  fourierdlem68  46529  fourierdlem73  46534  fourierdlem74  46535  fourierdlem75  46536  fourierdlem76  46537  fourierdlem78  46539  fourierdlem81  46542  fourierdlem82  46543  fourierdlem83  46544  fourierdlem84  46545  fourierdlem85  46546  fourierdlem88  46549  fourierdlem90  46551  fourierdlem92  46553  fourierdlem93  46554  fourierdlem95  46556  fourierdlem97  46558  fourierdlem101  46562  fourierdlem103  46564  fourierdlem104  46565  fourierdlem111  46572  fourierdlem112  46573  sqwvfoura  46583  sqwvfourb  46584  fouriersw  46586  elaa2lem  46588  etransclem4  46593  etransclem17  46606  etransclem18  46607  etransclem32  46621  etransclem46  46635  sge0z  46730  sge0revalmpt  46733  sge0tsms  46735  sge0sup  46746  sge0iunmptlemre  46770  sge0iun  46774  sge0xaddlem2  46789  ismeannd  46822  psmeasurelem  46825  meaiuninclem  46835  meaiininclem  46841  caratheodory  46883  isomenndlem  46885  ovnval  46896  hoicvrrex  46911  ovnlecvr  46913  ovncvrrp  46919  ovn0lem  46920  ovnsubaddlem1  46925  hoidmv1lelem2  46947  hoidmv1le  46949  hoidmvlelem3  46952  ovnhoilem2  46957  ovnhoi  46958  ovnlecvr2  46965  ovncvr2  46966  hspmbllem2  46982  ovolval2lem  46998  ovolval3  47002  ovolval5lem1  47007  ovolval5lem2  47008  ovnovollem1  47011  ovnovollem2  47012  vonioolem1  47035  vonicclem1  47038  vonct  47048  smflim  47132  smfinflem  47172  smflimsuplem5  47179  smfliminflem  47185  cfsetsnfsetfv  47414  fundcmpsurbijinjpreimafv  47764  fundcmpsurinjimaid  47768  fdmdifeqresdif  48699  ply1mulgsumlem2  48744  lincvalsc0  48778  linc0scn0  48780  lincdifsn  48781  lincsum  48786  lincscm  48787  lindslinindimp2lem4  48818  lindslinindsimp2lem5  48819  lincresunit3lem2  48837  1arymaptfo  49000  itcovalpclem1  49027  itcovalpclem2  49028  itcovalt2lem1  49032  itcovalt2lem2  49033  tposcurf1  49655  tposcurf2  49656  diag1  49660  fuco22  49695  fucocolem2  49710  fucocolem3  49711  fucocolem4  49712  fucoco  49713  fucolid  49717  fucorid  49718  postcofval  49720  precofval  49723  precofvalALT  49724  precofval2  49725  fucoppcco  49765  islmd  50021  iscmd  50022  aacllem  50157  amgmwlem  50158