Theorem mpteq2dva 5203

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

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1540   ∈ wcel 2109   ↦ cmpt 5191

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2702

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-sb 2066  df-clab 2709  df-cleq 2722  df-clel 2804  df-opab 5173  df-mpt 5192

This theorem is referenced by:  mpteq2dv  5204  mpteq2ia  5205  2fvcoidd  7275  offval  7665  offval2  7676  coof  7680  caofinvl  7688  caofcom  7693  caofass  7696  caofdi  7698  caofdir  7699  caonncan  7700  curry1  8086  curry2  8089  mpocurryd  8251  pw2f1olem  9050  mapxpen  9113  xpmapenlem  9114  cantnfp1  9641  cantnflem1d  9648  cantnflem1  9649  cnfcom2lem  9661  dfac12lem1  10104  seqof  14031  seqof2  14032  swrdswrd  14677  repswswrd  14756  repswrevw  14759  revco  14807  ccatco  14808  repsco  14813  ofccat  14942  lo1eq  15541  rlimeq  15542  lo1mul2  15602  o1dif  15603  lo1sub  15604  rlimdiv  15619  caucvgr  15649  sumeq1  15662  fsumrlim  15784  fsumo1  15785  climfsum  15793  geomulcvg  15849  vdwlem8  16966  prmgapprmo  17040  restid2  17400  pwsplusgval  17460  pwsmulrval  17461  pwsvscafval  17464  qusin  17514  xpsaddlem  17543  xpsvsca  17547  catidd  17648  fuclid  17938  fucrid  17939  fucass  17940  setcepi  18057  prf1st  18172  prf2nd  18173  1st2ndprf  18174  curfcl  18200  curfuncf  18206  diag2  18213  curf2ndf  18215  hof2val  18224  hofcllem  18226  hofcl  18227  yonedalem4a  18243  yonedalem4c  18245  yonedalem3b  18247  yonedainv  18249  yonffthlem  18250  prdssgrpd  18667  prdsidlem  18703  prdsmndd  18704  mhmvlin  18735  pwsco2mhm  18767  frmdup3lem  18800  frmdup3  18801  smndex1gid  18837  smndex1igid  18838  grpinvpropd  18954  prdsinvlem  18988  pwsinvg  18992  pwssub  18993  galactghm  19341  cayleylem1  19349  pmtrprfval  19424  sylow1lem2  19536  sylow3lem1  19564  efginvrel1  19665  frgpup3lem  19714  frgpup3  19715  prdscmnd  19798  iscyggen  19817  gsumval3  19844  gsumcllem  19845  gsumzsplit  19864  gsumsub  19885  gsummptf1o  19900  gsum2d  19909  gsum2d2  19911  gsumxp  19913  prdsgsum  19918  telgsumfz  19927  telgsumfz0  19929  telgsum  19931  dprdfsub  19960  dprdfeq0  19961  dprddisj2  19978  dprd2d2  19983  dpjidcl  19997  ablfaclem2  20025  ablfac2  20028  prdsmgp  20067  prdsrngd  20092  srgbinomlem3  20144  srgbinomlem4  20145  srgbinomlem  20146  gsumdixp  20235  prdsringd  20237  prdslmodd  20882  mulgrhm2  21395  frgpcyg  21490  freshmansdream  21491  evpmodpmf1o  21512  phlpropd  21571  frlmphl  21697  uvcresum  21709  frlmup1  21714  asclpropd  21813  psrass1lem  21848  psrlinv  21871  psrass1  21880  psrdi  21881  psrdir  21882  psrass23l  21883  psrcom  21884  psrass23  21885  resspsrmul  21892  mplsubrglem  21920  mplmonmul  21950  mplcoe1  21951  mplcoe5  21954  mplcoe4  21985  evlslem3  21994  evlslem1  21996  mhpmulcl  22043  psdmplcl  22056  psdadd  22057  psdmul  22060  psdmvr  22063  psrplusgpropd  22127  psropprmul  22129  coe1mul2  22162  coe1tm  22166  coe1tmmul2  22169  coe1tmmul  22170  coe1pwmul  22172  cply1mul  22190  ply1coe  22192  eqcoe1ply1eq  22193  lply1binomsc  22205  evl1gsummon  22259  evls1fpws  22263  rhmcomulmpl  22276  mamures  22291  grpvrinv  22293  mamuass  22296  mamudi  22297  mamudir  22298  mamuvs1  22299  mamuvs2  22300  mpomatmul  22340  mamutpos  22352  madetsumid  22355  dmatmul  22391  scmatscm  22407  1mavmul  22442  mavmulass  22443  mvmumamul1  22448  mulmarep1gsum1  22467  mulmarep1gsum2  22468  mdetleib2  22482  mdetfval1  22484  mdet0pr  22486  mdetdiag  22493  mdetdiagid  22494  mdetrlin  22496  mdetrsca  22497  mdetralt  22502  mdetunilem9  22514  gsummatr01  22553  smadiadetlem1a  22557  smadiadetlem3  22562  smadiadetlem4  22563  cpmatmcllem  22612  mat2pmatmul  22625  decpmatmullem  22665  decpmatmul  22666  pmatcollpw1lem2  22669  pmatcollpw  22675  pmatcollpw3lem  22677  pmatcollpwscmat  22685  idpm2idmp  22695  mp2pm2mplem3  22702  mp2pm2mplem4  22703  mp2pm2mplem5  22704  mp2pm2mp  22705  pm2mpghm  22710  pm2mpmhmlem2  22713  monmat2matmon  22718  pm2mp  22719  chpdmat  22735  chpscmat  22736  chpscmatgsumbin  22738  chpscmatgsummon  22739  chp0mat  22740  chpidmat  22741  chfacfscmulgsum  22754  chfacfpmmulgsum  22758  chfacfpmmulgsum2  22759  cayhamlem1  22760  cpmidgsumm2pm  22763  cpmidpmat  22767  cpmadugsumlemB  22768  cpmadugsumlemC  22769  cpmadugsumlemF  22770  cpmadumatpoly  22777  cayhamlem3  22781  cayhamlem4  22782  cayleyhamilton0  22783  cayleyhamiltonALT  22785  neiptopnei  23026  neiptopreu  23027  ptcnplem  23515  cnmpt1t  23559  cnmpt12  23561  cnmptkp  23574  cnmptk1  23575  cnmpt1k  23576  cnmptkk  23577  cnmptk1p  23579  cnmpt2k  23582  qtopeu  23610  pt1hmeo  23700  ptunhmeo  23702  xkocnv  23708  xkohmeo  23709  flfcnp2  23901  cnmpt1plusg  23981  istgp2  23985  tmdmulg  23986  tgpmulg  23987  tmdgsum  23989  subgtgp  23999  symgtgp  24000  tgpconncomp  24007  prdstgpd  24019  tsmsmhm  24040  tsmsadd  24041  tsmssub  24043  tgptsmscls  24044  tsmssplit  24046  tsmsxplem1  24047  tsmsxplem2  24048  cnmpt1vsca  24088  tlmtgp  24090  ustuqtoplem  24134  utopsnneip  24143  ressprdsds  24266  metuval  24444  nmfval0  24485  tngnm  24546  nmoeq0  24631  idnghm  24638  cnmpt1ds  24738  fsumcn  24768  expcn  24770  divccn  24771  expcnOLD  24772  divccnOLD  24773  divccncf  24806  negcncf  24822  negcncfOLD  24823  copco  24925  pcopt  24929  pcopt2  24930  pcoass  24931  pi1xfrcnvlem  24963  cnmpt1ip  25154  rrxnm  25298  rrxds  25300  minveclem3b  25335  divcncf  25355  ovolctb  25398  ovoliunnul  25415  voliunlem3  25460  ovolfs2  25479  uniioombllem2  25491  vitalilem4  25519  vitalilem5  25520  ismbf  25536  mbfss  25554  mbfmulc2re  25556  mbfneg  25558  mbfpos  25559  mbfposb  25561  mbfadd  25569  mbfsub  25570  mbfmulc2  25571  mbfinf  25573  mbflimsup  25574  mbflimlem  25575  i1fpos  25614  i1fposd  25615  itg1climres  25622  mbfmul  25634  itg2mulc  25655  itg2i1fseq  25663  itg2cnlem1  25669  itg2cnlem2  25670  itgresr  25687  iblneg  25711  i1fibl  25716  itgitg1  25717  iblsub  25730  itgfsum  25735  itgmulc2lem1  25740  limcmpt  25791  limccnp  25799  limcco  25801  dvreslem  25817  dvres2lem  25818  dvidlem  25823  dvcnp2  25828  dvcnp2OLD  25829  dvaddbr  25847  dvmulbr  25848  dvmulbrOLD  25849  dvmulf  25853  dvcmulf  25855  dvcobr  25856  dvcobrOLD  25857  dvcof  25859  dvcjbr  25860  dvcj  25861  dvfre  25862  dvexp  25864  dvexp2  25865  dvrec  25866  dvmptcmul  25875  dvmptdivc  25876  dvmptneg  25877  dvmptsub  25878  dvmptre  25880  dvmptim  25881  dvrecg  25884  dvmptdiv  25885  dvmptfsum  25886  dvcnvlem  25887  dvcnv  25888  dvexp3  25889  dvef  25891  dvsincos  25892  dv11cn  25913  lhop2  25927  lhop  25928  ftc2  25958  itgparts  25961  itgsubstlem  25962  mdegfval  25974  mdegmullem  25990  ply1termlem  26115  plypow  26117  plyconst  26118  plyeq0lem  26122  plypf1  26124  plyaddlem1  26125  plymullem1  26126  coeeulem  26136  coeidlem  26149  plyco  26153  coeeq2  26154  0dgr  26157  0dgrb  26158  dgrcolem1  26186  dgrcolem2  26187  plycjlem  26189  dvply1  26198  dvply2g  26199  dvply2gOLD  26200  plydiveu  26213  plyremlem  26219  elqaalem3  26236  taylfval  26273  dvtaylp  26285  taylthlem1  26288  taylthlem2  26289  taylthlem2OLD  26290  ulmshft  26306  mtestbdd  26321  iblulm  26323  itgulm2  26325  pserulm  26338  psercn2  26339  psercn2OLD  26340  pserdvlem2  26345  pserdv  26346  pserdv2  26347  abelthlem1  26348  abelthlem3  26350  advlog  26570  advlogexp  26571  dvcxp1  26656  dvcxp2  26657  dvcncxp1  26659  sqrtcn  26667  loglesqrt  26678  dvatan  26852  atantayl2  26855  atantayl3  26856  leibpi  26859  rlimcnp2  26883  efrlim  26886  efrlimOLD  26887  dfef2  26888  cxp2lim  26894  divsqrtsumlem  26897  lgamgulmlem2  26947  lgamgulm2  26953  lgamcvglem  26957  gamcvg2lem  26976  ftalem7  26996  basellem9  27006  muinv  27110  logfacrlim  27142  logexprlim  27143  dchrmullid  27170  dchrinvcl  27171  lgseisenlem3  27295  lgseisenlem4  27296  chtppilimlem2  27392  chebbnd2  27395  chpchtlim  27397  chpo1ub  27398  rpvmasumlem  27405  dchrmusumlema  27411  dchrvmasumlem1  27413  dchrvmasumiflem2  27420  dchrisum0fno1  27429  rpvmasum2  27430  dchrisum0lema  27432  dchrisum0lem1  27434  dchrisum0lem2a  27435  dchrisum0lem2  27436  dchrisum0  27438  dchrmusumlem  27440  dchrvmasumlem  27441  rpvmasum  27444  rplogsum  27445  logdivsum  27451  mulog2sumlem3  27454  vmalogdivsum2  27456  vmalogdivsum  27457  2vmadivsumlem  27458  logsqvma2  27461  log2sumbnd  27462  selberglem2  27464  selberg3lem1  27475  selberg3  27477  selberg4lem1  27478  selberg4  27479  pntrsumo1  27483  selberg3r  27487  selberg4r  27488  selberg34r  27489  pntrlog2bndlem2  27496  pntrlog2bndlem4  27498  pntrlog2bndlem5  27499  pntrlog2bndlem6  27501  padicabvf  27549  padicabvcxp  27550  mirval  28589  crctcshlem4  29757  clwlknf1oclwwlkn  30020  eucrct2eupth  30181  chscllem4  31576  brafnmul  31887  kbmul  31891  cofmpt2  32565  ofresid  32573  ofoprabco  32595  fmptunsnop  32630  fcobijfs  32653  gsummpt2d  32996  gsummptres  32999  gsummptres2  33000  gsummptfsf1o  33001  gsumfs2d  33002  gsumpart  33004  gsumhashmul  33008  gsumwrd2dccat  33014  fzto1st1  33066  fzto1st  33067  elrgspnlem1  33200  elrgspnlem2  33201  elrgspnlem3  33202  elrgspnlem4  33203  elrgspnsubrunlem1  33205  elrgspnsubrunlem2  33206  qusbas2  33384  qusima  33386  elrspunidl  33406  elrspunsn  33407  rprmdvdsprod  33512  ressply1evls1  33541  evl1deg1  33552  evl1deg2  33553  evl1deg3  33554  gsummoncoe1fzo  33570  lbsdiflsp0  33629  fedgmullem1  33632  fedgmullem2  33633  fldextrspunlsplem  33675  fldextrspunlsp  33676  mdetpmtr1  33820  mdetlap  33829  xrge0mulc1cn  33938  esumval  34043  esumsnf  34061  esumpcvgval  34075  esumcvg  34083  esumcvgsum  34085  esumsup  34086  ofcfeqd2  34098  meascnbl  34216  sitgval  34330  probmeasb  34428  cndprobprob  34436  dstfrvclim1  34476  ballotlemfval  34488  ballotlemsval  34507  ballotlemieq  34515  plymul02  34544  plymulx0  34545  plymulx  34546  signsplypnf  34548  signstfv  34561  signstfvn  34567  signstfvp  34569  itgexpif  34604  logdivsqrle  34648  ptpconn  35227  cvmliftlem6  35284  cvmliftphtlem  35311  cvmlift3lem5  35317  elmrsubrn  35514  msubfval  35518  msubco  35525  divcnvlin  35727  knoppcnlem9  36496  knoppcnlem10  36497  knoppcnlem11  36498  bj-finsumval0  37280  curf  37599  matunitlindflem1  37617  matunitlindflem2  37618  poimirlem3  37624  poimirlem15  37636  poimirlem16  37637  poimirlem17  37638  poimirlem19  37640  poimirlem20  37641  broucube  37655  ovoliunnfl  37663  voliunnfl  37665  volsupnfl  37666  mbfposadd  37668  itg2addnclem  37672  itg2addnclem3  37674  itg2addnc  37675  itgaddnclem2  37680  itgaddnc  37681  iblsubnc  37682  itgsubnc  37683  itgmulc2nclem1  37687  itgmulc2nclem2  37688  itgmulc2nc  37689  itgabsnc  37690  ftc1cnnclem  37692  ftc1anclem3  37696  ftc1anclem5  37698  ftc1anclem6  37699  ftc1anclem8  37701  ftc1anc  37702  ftc2nc  37703  areacirclem1  37709  areacirclem2  37710  areacirclem4  37712  areacirc  37714  upixp  37730  lcmineqlem8  42031  lcmineqlem12  42035  dvrelog2b  42061  dvrelogpow2b  42063  aks4d1p1p6  42068  aks4d1p1p5  42070  aks6d1c1  42111  aks6d1c5lem3  42132  sticksstones12a  42152  sticksstones12  42153  sticksstones19  42160  aks6d1c6lem1  42165  aks6d1c6lem4  42168  aks6d1c7lem3  42177  qsalrel  42235  pwsgprod  42539  rhmcomulpsr  42546  evlsvvval  42558  evlsevl  42566  selvvvval  42580  evlselv  42582  fsuppssindlem1  42586  fsuppssind  42588  mhphf  42592  mzpsubst  42743  mzprename  42744  mzpcompact2lem  42746  eldioph2  42757  rabdiophlem2  42797  mendlmod  43185  mendassa  43186  areaquad  43212  fsovcnvlem  44009  hashnzfzclim  44318  expgrowthi  44329  expgrowth  44331  uzmptshftfval  44342  dvradcnv2  44343  binomcxplemrat  44346  binomcxplemfrat  44347  binomcxplemradcnv  44348  binomcxplemdvbinom  44349  binomcxplemcvg  44350  binomcxplemdvsum  44351  binomcxplemnotnn0  44352  mulc1cncfg  45594  expcnfg  45596  fprodcnlem  45604  clim1fr1  45606  divcnvg  45632  sublimc  45657  reclimc  45658  divlimc  45661  limsupresico  45705  limsuppnfdlem  45706  limsupvaluz  45713  supcnvlimsupmpt  45746  liminfresico  45776  climliminflimsupd  45806  cncfmptssg  45876  negcncfg  45886  cncficcgt0  45893  fprodcncf  45905  fprodsubrecnncnvlem  45912  fprodaddrecnncnvlem  45914  dvsinax  45918  dvasinbx  45925  dvdivf  45927  ioodvbdlimc1lem2  45937  ioodvbdlimc2lem  45939  dvnmptdivc  45943  dvxpaek  45945  dvnxpaek  45947  dvnmul  45948  dvnprodlem2  45952  ibliccsinexp  45956  itgsinexplem1  45959  itgsinexp  45960  iblempty  45970  itgcoscmulx  45974  itgsincmulx  45979  itgioocnicc  45982  iblcncfioo  45983  itgsbtaddcnst  45987  volioofmpt  45999  volicofmpt  46002  stoweidlem4  46009  stirlinglem5  46083  dirkerval  46096  dirkertrigeq  46106  dirkeritg  46107  dirkercncflem2  46109  dirkercncflem4  46111  fourierdlem16  46128  fourierdlem18  46130  fourierdlem21  46133  fourierdlem22  46134  fourierdlem28  46140  fourierdlem39  46151  fourierdlem40  46152  fourierdlem41  46153  fourierdlem53  46164  fourierdlem56  46167  fourierdlem57  46168  fourierdlem60  46171  fourierdlem61  46172  fourierdlem68  46179  fourierdlem73  46184  fourierdlem74  46185  fourierdlem75  46186  fourierdlem76  46187  fourierdlem78  46189  fourierdlem81  46192  fourierdlem82  46193  fourierdlem83  46194  fourierdlem84  46195  fourierdlem85  46196  fourierdlem88  46199  fourierdlem90  46201  fourierdlem92  46203  fourierdlem93  46204  fourierdlem95  46206  fourierdlem97  46208  fourierdlem101  46212  fourierdlem103  46214  fourierdlem104  46215  fourierdlem111  46222  fourierdlem112  46223  sqwvfoura  46233  sqwvfourb  46234  fouriersw  46236  elaa2lem  46238  etransclem4  46243  etransclem17  46256  etransclem18  46257  etransclem32  46271  etransclem46  46285  sge0z  46380  sge0revalmpt  46383  sge0tsms  46385  sge0sup  46396  sge0iunmptlemre  46420  sge0iun  46424  sge0xaddlem2  46439  ismeannd  46472  psmeasurelem  46475  meaiuninclem  46485  meaiininclem  46491  caratheodory  46533  isomenndlem  46535  ovnval  46546  hoicvrrex  46561  ovnlecvr  46563  ovncvrrp  46569  ovn0lem  46570  ovnsubaddlem1  46575  hoidmv1lelem2  46597  hoidmv1le  46599  hoidmvlelem3  46602  ovnhoilem2  46607  ovnhoi  46608  ovnlecvr2  46615  ovncvr2  46616  hspmbllem2  46632  ovolval2lem  46648  ovolval3  46652  ovolval5lem1  46657  ovolval5lem2  46658  ovnovollem1  46661  ovnovollem2  46662  vonioolem1  46685  vonicclem1  46688  vonct  46698  smflim  46782  smfinflem  46822  smflimsuplem5  46829  smfliminflem  46835  cfsetsnfsetfv  47062  fundcmpsurbijinjpreimafv  47412  fundcmpsurinjimaid  47416  fdmdifeqresdif  48334  ply1mulgsumlem2  48380  lincvalsc0  48414  linc0scn0  48416  lincdifsn  48417  lincsum  48422  lincscm  48423  lindslinindimp2lem4  48454  lindslinindsimp2lem5  48455  lincresunit3lem2  48473  1arymaptfo  48636  itcovalpclem1  48663  itcovalpclem2  48664  itcovalt2lem1  48668  itcovalt2lem2  48669  tposcurf1  49292  tposcurf2  49293  diag1  49297  fuco22  49332  fucocolem2  49347  fucocolem3  49348  fucocolem4  49349  fucoco  49350  fucolid  49354  fucorid  49355  postcofval  49357  precofval  49360  precofvalALT  49361  precofval2  49362  fucoppcco  49402  islmd  49658  iscmd  49659  aacllem  49794  amgmwlem  49795