Theorem mpteq2dva 5198

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

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

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 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2733

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-sb 2100  df-clab 2740  df-cleq 2753  df-clel 2836  df-opab 5168  df-mpt 5187

This theorem is used by:  mpteq2dv  5199  mpteq2ia  5200  2fvcoidd  7303  offval  7700  offval2  7711  coof  7715  caofinvl  7723  caofcom  7728  caofass  7731  caofdi  7733  caofdir  7734  caonncan  7735  curry1  8113  curry2  8116  mpocurryd  8279  curf  8883  pw2f1olem  9093  mapxpen  9155  xpmapenlem  9156  cantnfp1  9675  cantnflem1d  9682  cantnflem1  9683  cnfcom2lem  9695  dfac12lem1  10215  seqof  14195  seqof2  14196  swrdswrd  14847  repswswrd  14928  repswrevw  14931  revco  14978  ccatco  14979  repsco  14984  ofccat  15115  lo1eq  15728  rlimeq  15729  lo1mul2  15789  o1dif  15790  lo1sub  15791  rlimdiv  15806  caucvgr  15836  sumeq1  15849  fsumrlim  15971  fsumo1  15972  climfsum  15980  geomulcvg  16038  vdwlem8  17159  prmgapprmo  17233  restid2  17594  pwsplusgval  17655  pwsmulrval  17656  pwsvscafval  17659  qusin  17709  xpsaddlem  17738  xpsvsca  17742  catidd  17847  fuclid  18137  fucrid  18138  fucass  18139  setcepi  18256  prf1st  18371  prf2nd  18372  1st2ndprf  18373  curfcl  18399  curfuncf  18405  diag2  18412  curf2ndf  18414  hof2val  18423  hofcllem  18425  hofcl  18426  yonedalem4a  18442  yonedalem4c  18444  yonedalem3b  18446  yonedainv  18448  yonffthlem  18449  prdssgrpd  18915  prdsidlem  18956  prdsmndd  18957  mhmvlin  18989  pwsco2mhm  19022  frmdup3lem  19055  frmdup3  19056  smndex1gid  19093  smndex1gidOLD  19094  smndex1igidOLD  19096  grpinvpropd  19218  prdsinvlem  19252  pwsinvg  19256  pwssub  19257  galactghm  19611  cayleylem1  19619  pmtrprfval  19694  sylow1lem2  19806  sylow3lem1  19834  efginvrel1  19935  frgpup3lem  19984  frgpup3  19985  prdscmnd  20068  iscyggen  20087  gsumval3  20114  gsumcllem  20115  gsumzsplit  20134  gsumsub  20155  gsummptf1o  20170  gsum2d  20179  gsum2d2  20181  gsumxp  20183  prdsgsum  20188  telgsumfz  20197  telgsumfz0  20199  telgsum  20201  dprdfsub  20230  dprdfeq0  20231  dprddisj2  20248  dprd2d2  20253  dpjidcl  20267  ablfaclem2  20295  ablfac2  20298  prdsmgp  20364  prdsrngd  20391  srgbinomlem3  20447  srgbinomlem4  20448  srgbinomlem  20449  gsumdixp  20541  prdsringd  20543  pwsgprod  20552  prdslmodd  21237  mulgrhm2  21777  frgpcyg  21872  freshmansdream  21873  evpmodpmf1o  21895  phlpropd  21954  frlmphl  22080  uvcresum  22092  frlmup1  22097  asclpropd  22198  psrass1lem  22234  psrlinv  22256  psrass1  22264  psrdi  22265  psrdir  22266  psrass23l  22267  psrcom  22268  psrass23  22269  resspsrmul  22276  mplsubrglem  22304  mplmonmul  22338  mplcoe1  22339  mplcoe5  22342  mplcoe4  22373  evlslem3  22382  evlslem1  22384  evlsvvval  22395  rhmcomulmpl  22426  evlsevl  22434  selvvvval  22444  mhpmulcl  22463  psdmplcl  22476  psdadd  22477  psdmul  22480  psdmvr  22483  psrplusgpropd  22546  psropprmul  22548  coe1mul2  22581  coe1tm  22585  coe1tmmul2  22588  coe1tmmul  22589  coe1pwmul  22591  cply1mul  22607  ply1coe  22609  eqcoe1ply1eq  22610  lply1binomsc  22622  evl1gsummon  22676  evls1fpws  22680  mamures  22705  grpvrinv  22707  mamuass  22710  mamudi  22711  mamudir  22712  mamuvs1  22713  mamuvs2  22714  mpomatmul  22754  mamutpos  22766  madetsumid  22769  dmatmul  22805  scmatscm  22821  1mavmul  22856  mavmulass  22857  mvmumamul1  22862  mulmarep1gsum1  22881  mulmarep1gsum2  22882  mdetleib2  22896  mdetfval1  22898  mdet0pr  22900  mdetdiag  22907  mdetdiagid  22908  mdetrlin  22910  mdetrsca  22911  mdetralt  22916  mdetunilem9  22928  gsummatr01  22967  smadiadetlem1a  22971  smadiadetlem3  22976  smadiadetlem4  22977  matunitlindflem1  22987  matunitlindflem2  22988  cpmatmcllem  23029  mat2pmatmul  23042  decpmatmullem  23082  decpmatmul  23083  pmatcollpw1lem2  23086  pmatcollpw  23092  pmatcollpw3lem  23094  pmatcollpwscmat  23102  idpm2idmp  23112  mp2pm2mplem3  23119  mp2pm2mplem4  23120  mp2pm2mplem5  23121  mp2pm2mp  23122  pm2mpghm  23127  pm2mpmhmlem2  23130  monmat2matmon  23135  pm2mp  23136  chpdmat  23152  chpscmat  23153  chpscmatgsumbin  23155  chpscmatgsummon  23156  chp0mat  23157  chpidmat  23158  chfacfscmulgsum  23171  chfacfpmmulgsum  23175  chfacfpmmulgsum2  23176  cayhamlem1  23177  cpmidgsumm2pm  23180  cpmidpmat  23184  cpmadugsumlemB  23185  cpmadugsumlemC  23186  cpmadugsumlemF  23187  cpmadumatpoly  23194  cayhamlem3  23198  cayhamlem4  23199  cayleyhamilton0  23200  cayleyhamiltonALT  23202  neiptopnei  23443  neiptopreu  23444  ptcnplem  23933  cnmpt1t  23977  cnmpt12  23979  cnmptkp  23992  cnmptk1  23993  cnmpt1k  23994  cnmptkk  23995  cnmptk1p  23997  cnmpt2k  24000  qtopeu  24028  pt1hmeo  24118  ptunhmeo  24120  xkocnv  24126  xkohmeo  24127  flfcnp2  24319  cnmpt1plusg  24399  istgp2  24403  tmdmulg  24404  tgpmulg  24405  tmdgsum  24407  subgtgp  24417  symgtgp  24418  tgpconncomp  24425  prdstgpd  24437  tsmsmhm  24458  tsmsadd  24459  tsmssub  24461  tgptsmscls  24462  tsmssplit  24464  tsmsxplem1  24465  tsmsxplem2  24466  cnmpt1vsca  24506  tlmtgp  24508  ustuqtoplem  24551  utopsnneip  24560  ressprdsds  24683  metuval  24861  nmfval0  24902  tngnm  24963  nmoeq0  25048  idnghm  25055  cnmpt1ds  25155  fsumcn  25184  expcn  25186  divccn  25187  divccncf  25220  negcncf  25236  copco  25332  pcopt  25336  pcopt2  25337  pcoass  25338  pi1xfrcnvlem  25370  cnmpt1ip  25561  rrxnm  25705  rrxds  25707  minveclem3b  25742  divcncf  25761  ovolctb  25804  ovoliunnul  25821  voliunlem3  25866  ovolfs2  25885  uniioombllem2  25897  vitalilem4  25925  vitalilem5  25926  ismbf  25942  mbfss  25960  mbfmulc2re  25962  mbfneg  25964  mbfpos  25965  mbfposb  25967  mbfadd  25975  mbfsub  25976  mbfmulc2  25977  mbfinf  25979  mbflimsup  25980  mbflimlem  25981  i1fpos  26020  i1fposd  26021  itg1climres  26028  mbfmul  26040  itg2mulc  26061  itg2i1fseq  26069  itg2cnlem1  26075  itg2cnlem2  26076  itgresr  26092  iblneg  26116  i1fibl  26121  itgitg1  26122  iblsub  26135  itgfsum  26140  itgmulc2lem1  26145  limcmpt  26196  limccnp  26204  limcco  26206  dvreslem  26222  dvres2lem  26223  dvidlem  26228  dvcnp2  26233  dvaddbr  26251  dvmulbr  26252  dvmulf  26256  dvcmulf  26258  dvcobr  26259  dvcof  26261  dvcjbr  26262  dvcj  26263  dvfre  26264  dvexp  26266  dvexp2  26267  dvrec  26268  dvmptcmul  26277  dvmptdivc  26278  dvmptneg  26279  dvmptsub  26280  dvmptre  26282  dvmptim  26283  dvrecg  26286  dvmptdiv  26287  dvmptfsum  26288  dvcnvlem  26289  dvcnv  26290  dvexp3  26291  dvef  26293  dvsincos  26294  dv11cn  26314  lhop2  26328  lhop  26329  ftc2  26357  itgparts  26360  itgsubstlem  26361  mdegfval  26373  mdegmullem  26389  ply1termlem  26514  plypow  26516  plyconst  26517  plyeq0lem  26522  plypf1  26524  plyaddlem1  26525  plymullem1  26526  coeeulem  26536  coeidlem  26549  plyco  26553  coeeq2  26554  0dgr  26557  0dgrb  26558  dgrcolem1  26585  dgrcolem2  26586  plycjlem  26588  plymul02  26594  plyn0mulidp  26595  plymulidp  26596  dvply1  26598  dvply2g  26599  plydiveu  26612  plyremlem  26618  elqaalem3  26637  taylfval  26679  dvtaylp  26690  taylthlem1  26693  taylthlem2  26694  ulmshft  26710  mtestbdd  26725  iblulm  26727  itgulm2  26729  pserulm  26742  psercn2  26743  pserdvlem2  26748  pserdv  26749  pserdv2  26750  abelthlem1  26751  abelthlem3  26753  advlog  26975  advlogexp  26976  dvcxp1  27061  dvcxp2  27062  dvcncxp1  27064  sqrtcn  27071  loglesqrt  27082  dvatan  27256  atantayl2  27259  atantayl3  27260  leibpi  27263  rlimcnp2  27287  efrlim  27290  dfef2  27291  cxp2lim  27297  divsqrtsumlem  27300  lgamgulmlem2  27350  lgamgulm2  27356  lgamcvglem  27360  gamcvg2lem  27379  ftalem7  27399  basellem9  27409  muinv  27513  logfacrlim  27544  logexprlim  27545  dchrmullid  27572  dchrinvcl  27573  lgseisenlem3  27697  lgseisenlem4  27698  chtppilimlem2  27794  chebbnd2  27797  chpchtlim  27799  chpo1ub  27800  rpvmasumlem  27807  dchrmusumlema  27813  dchrvmasumlem1  27815  dchrvmasumiflem2  27822  dchrisum0fno1  27831  rpvmasum2  27832  dchrisum0lema  27834  dchrisum0lem1  27836  dchrisum0lem2a  27837  dchrisum0lem2  27838  dchrisum0  27840  dchrmusumlem  27842  dchrvmasumlem  27843  rpvmasum  27846  rplogsum  27847  logdivsum  27853  mulog2sumlem3  27856  vmalogdivsum2  27858  vmalogdivsum  27859  2vmadivsumlem  27860  logsqvma2  27863  log2sumbnd  27864  selberglem2  27866  selberg3lem1  27877  selberg3  27879  selberg4lem1  27880  selberg4  27881  pntrsumo1  27885  selberg3r  27889  selberg4r  27890  selberg34r  27891  pntrlog2bndlem2  27898  pntrlog2bndlem4  27900  pntrlog2bndlem5  27901  pntrlog2bndlem6  27903  padicabvf  27951  padicabvcxp  27952  mirval  29120  crctcshlem4  30402  clwlknf1oclwwlkn  30668  eucrct2eupth  30839  chscllem4  32235  brafnmul  32546  kbmul  32550  cofmpt2  33221  ofresid  33229  ofoprabco  33251  fmptunsnop  33286  fcobijfs  33306  fcobijfs2  33307  gsummpt2d  33603  gsummptres  33606  gsummptres2  33607  gsummptf1od  33609  gsummptp1  33611  gsummptfsf1o  33614  gsumfs2d  33615  gsumpart  33617  gsumhashmul  33621  gsummulsubdishift1  33622  gsummulsubdishift2  33623  gsumwrd2dccat  33632  fzto1st1  33656  fzto1st  33657  elrgspnlem1  33796  elrgspnlem2  33797  elrgspnlem3  33798  elrgspnlem4  33799  elrgspnsubrunlem1  33801  elrgspnsubrunlem2  33802  qusbas2  33950  qusima  33952  elrspunidl  33971  elrspunsn  33972  rprmdvdsprod  34059  ressply1evls1  34090  evl1deg1  34101  evl1deg2  34102  evl1deg3  34103  gsummoncoe1fzo  34122  mplasclco  34141  selvply1rhmlemb  34144  selvply1rhmlem2  34146  selvply1rhmlem4  34148  selvply1rhm0  34151  mplmulmvr  34164  evlextv  34167  mplvrpmga  34170  mplvrpmmhm  34171  mplvrpmrhm  34172  psrgsum  34173  psrmonmul  34175  issply  34186  esplyfval0  34189  esplyfval3  34197  esplyfval1  34198  esplyfvaln  34199  esplyind  34200  vietalem  34204  lbsdiflsp0  34251  fedgmullem1  34254  fedgmullem2  34255  fldextrspunlsplem  34298  fldextrspunlsp  34299  extdgfialglem2  34318  mdetpmtr1  34448  mdetlap  34457  xrge0mulc1cn  34566  esumval  34671  esumsnf  34689  esumpcvgval  34703  esumcvg  34711  esumcvgsum  34713  esumsup  34714  ofcfeqd2  34726  meascnbl  34845  sitgval  34957  probmeasb  35055  cndprobprob  35063  dstfrvclim1  35103  ballotlemfval  35115  ballotlemsval  35134  ballotlemieq  35142  signsplypnf  35172  signstfv  35185  signstfvn  35191  signstfvp  35193  itgexpif  35228  logdivsqrle  35272  ptpconn  35977  cvmliftlem6  36034  cvmliftphtlem  36061  cvmlift3lem5  36067  elmrsubrn  36264  msubfval  36268  msubco  36275  divcnvlin  36477  knoppcnlem9  37347  knoppcnlem10  37348  knoppcnlem11  37349  bj-finsumval0  38186  poimirlem3  38521  poimirlem15  38533  poimirlem16  38534  poimirlem17  38535  poimirlem19  38537  poimirlem20  38538  broucube  38552  ovoliunnfl  38560  voliunnfl  38562  volsupnfl  38563  mbfposadd  38565  itg2addnclem  38569  itg2addnclem3  38571  itg2addnc  38572  itgaddnclem2  38577  itgaddnc  38578  iblsubnc  38579  itgsubnc  38580  itgmulc2nclem1  38584  itgmulc2nclem2  38585  itgmulc2nc  38586  itgabsnc  38587  ftc1cnnclem  38589  ftc1anclem3  38593  ftc1anclem5  38595  ftc1anclem6  38596  ftc1anclem8  38598  ftc1anc  38599  ftc2nc  38600  areacirclem1  38606  areacirclem2  38607  areacirclem4  38609  areacirc  38611  upixp  38643  lcmineqlem8  43066  lcmineqlem12  43070  dvrelog2b  43096  dvrelogpow2b  43098  aks4d1p1p6  43103  aks4d1p1p5  43105  aks6d1c1  43146  aks6d1c5lem3  43167  sticksstones12a  43187  sticksstones12  43188  sticksstones19  43195  aks6d1c6lem1  43200  aks6d1c6lem4  43203  aks6d1c7lem3  43212  qsalrel  43272  rhmcomulpsr  43590  evlselv  43597  fsuppssindlem1  43599  fsuppssind  43601  mhphf  43605  mzpsubst  43738  mzprename  43739  mzpcompact2lem  43741  eldioph2  43752  rabdiophlem2  43788  mendlmod  44175  mendassa  44176  areaquad  44202  fsovcnvlem  44998  hashnzfzclim  45291  expgrowthi  45302  expgrowth  45304  uzmptshftfval  45315  dvradcnv2  45316  binomcxplemrat  45319  binomcxplemfrat  45320  binomcxplemradcnv  45321  binomcxplemdvbinom  45322  binomcxplemcvg  45323  binomcxplemdvsum  45324  binomcxplemnotnn0  45325  mulc1cncfg  46570  expcnfg  46572  fprodcnlem  46580  clim1fr1  46582  divcnvg  46608  sublimc  46631  reclimc  46632  divlimc  46635  limsupresico  46679  limsuppnfdlem  46680  limsupvaluz  46687  supcnvlimsupmpt  46720  liminfresico  46750  climliminflimsupd  46780  cncfmptssg  46850  negcncfg  46860  cncficcgt0  46867  fprodcncf  46879  fprodsubrecnncnvlem  46886  fprodaddrecnncnvlem  46888  dvsinax  46892  dvasinbx  46899  dvdivf  46901  ioodvbdlimc1lem2  46911  ioodvbdlimc2lem  46913  dvnmptdivc  46917  dvxpaek  46919  dvnxpaek  46921  dvnmul  46922  dvnprodlem2  46926  ibliccsinexp  46930  itgsinexplem1  46933  itgsinexp  46934  iblempty  46944  itgcoscmulx  46948  itgsincmulx  46953  itgioocnicc  46956  iblcncfioo  46957  itgsbtaddcnst  46961  volioofmpt  46973  volicofmpt  46976  stoweidlem4  46983  stirlinglem5  47057  dirkerval  47070  dirkertrigeq  47080  dirkeritg  47081  dirkercncflem2  47083  dirkercncflem4  47085  fourierdlem16  47102  fourierdlem18  47104  fourierdlem21  47107  fourierdlem22  47108  fourierdlem28  47114  fourierdlem39  47125  fourierdlem40  47126  fourierdlem41  47127  fourierdlem53  47138  fourierdlem56  47141  fourierdlem57  47142  fourierdlem60  47145  fourierdlem61  47146  fourierdlem68  47153  fourierdlem73  47158  fourierdlem74  47159  fourierdlem75  47160  fourierdlem76  47161  fourierdlem78  47163  fourierdlem81  47166  fourierdlem82  47167  fourierdlem83  47168  fourierdlem84  47169  fourierdlem85  47170  fourierdlem88  47173  fourierdlem90  47175  fourierdlem92  47177  fourierdlem93  47178  fourierdlem95  47180  fourierdlem97  47182  fourierdlem101  47186  fourierdlem103  47188  fourierdlem104  47189  fourierdlem111  47196  fourierdlem112  47197  sqwvfoura  47207  sqwvfourb  47208  fouriersw  47210  elaa2lem  47212  etransclem4  47217  etransclem17  47230  etransclem18  47231  etransclem32  47245  etransclem46  47259  sge0z  47354  sge0revalmpt  47357  sge0tsms  47359  sge0sup  47370  sge0iunmptlemre  47394  sge0iun  47398  sge0xaddlem2  47413  ismeannd  47446  psmeasurelem  47449  meaiuninclem  47459  meaiininclem  47465  caratheodory  47507  isomenndlem  47509  ovnval  47520  hoicvrrex  47535  ovnlecvr  47537  ovncvrrp  47543  ovn0lem  47544  ovnsubaddlem1  47549  hoidmv1lelem2  47571  hoidmv1le  47573  hoidmvlelem3  47576  ovnhoilem2  47581  ovnhoi  47582  ovnlecvr2  47589  ovncvr2  47590  hspmbllem2  47606  ovolval2lem  47622  ovolval3  47626  ovolval5lem1  47631  ovolval5lem2  47632  ovnovollem1  47635  ovnovollem2  47636  vonioolem1  47659  vonicclem1  47662  vonct  47672  smflim  47756  smfinflem  47796  smflimsuplem5  47803  smfliminflem  47809  cfsetsnfsetfv  48096  fundcmpsurbijinjpreimafv  48458  fundcmpsurinjimaid  48462  fdmdifeqresdif  49423  ply1mulgsumlem2  49468  lincvalsc0  49502  linc0scn0  49504  lincdifsn  49505  lincsum  49510  lincscm  49511  lindslinindimp2lem4  49542  lindslinindsimp2lem5  49543  lincresunit3lem2  49561  1arymaptfo  49724  itcovalpclem1  49751  itcovalpclem2  49752  itcovalt2lem1  49756  itcovalt2lem2  49757  tposcurf1  50376  tposcurf2  50377  diag1  50381  fuco22  50416  fucocolem2  50431  fucocolem3  50432  fucocolem4  50433  fucoco  50434  fucolid  50438  fucorid  50439  postcofval  50441  precofval  50444  precofvalALT  50445  precofval2  50446  fucoppcco  50486  islmd  50742  iscmd  50743  aacllem  50908  veronesematrowd  50950  veronesematrowexpd  50951  veroquadmodzerod  50953  amgmwlem  50956