Theorem mpteq2dva 5248

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 5237	1 ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵) = (𝑥 ∈ 𝐴 ↦ 𝐶))

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

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 5211  df-mpt 5232

This theorem is referenced by:  mpteq2dv  5250  mpteq2ia  5251  2fvcoidd  7297  offval  7681  offval2  7692  caofinvl  7702  caofcom  7707  caofass  7709  caofdi  7711  caofdir  7712  caonncan  7713  curry1  8092  curry2  8095  mpocurryd  8256  pw2f1olem  9078  mapxpen  9145  xpmapenlem  9146  cantnfp1  9678  cantnflem1d  9685  cantnflem1  9686  cnfcom2lem  9698  dfac12lem1  10140  seqof  14027  seqof2  14028  swrdswrd  14657  repswswrd  14736  repswrevw  14739  revco  14787  ccatco  14788  repsco  14793  ofccat  14918  lo1eq  15514  rlimeq  15515  lo1mul2  15575  o1dif  15576  lo1sub  15577  rlimdiv  15594  caucvgr  15624  sumeq1  15637  fsumrlim  15759  fsumo1  15760  climfsum  15768  geomulcvg  15824  vdwlem8  16923  prmgapprmo  16997  restid2  17378  pwsplusgval  17438  pwsmulrval  17439  pwsvscafval  17442  qusin  17492  xpsaddlem  17521  xpsvsca  17525  catidd  17626  fuclid  17921  fucrid  17922  fucass  17923  setcepi  18040  prf1st  18158  prf2nd  18159  1st2ndprf  18160  curfcl  18187  curfuncf  18193  diag2  18200  curf2ndf  18202  hof2val  18211  hofcllem  18213  hofcl  18214  yonedalem4a  18230  yonedalem4c  18232  yonedalem3b  18234  yonedainv  18236  yonffthlem  18237  prdssgrpd  18626  prdsidlem  18659  prdsmndd  18660  pwsco2mhm  18716  frmdup3lem  18749  frmdup3  18750  smndex1gid  18786  smndex1igid  18787  grpinvpropd  18900  prdsinvlem  18934  pwsinvg  18938  pwssub  18939  galactghm  19274  cayleylem1  19282  pmtrprfval  19357  sylow1lem2  19469  sylow3lem1  19497  efginvrel1  19598  frgpup3lem  19647  frgpup3  19648  prdscmnd  19731  iscyggen  19750  gsumval3  19777  gsumcllem  19778  gsumzsplit  19797  gsumsub  19818  gsummptf1o  19833  gsum2d  19842  gsum2d2  19844  gsumxp  19846  prdsgsum  19851  telgsumfz  19860  telgsumfz0  19862  telgsum  19864  dprdfsub  19893  dprdfeq0  19894  dprddisj2  19911  dprd2d2  19916  dpjidcl  19930  ablfaclem2  19958  ablfac2  19961  srgbinomlem3  20053  srgbinomlem4  20054  srgbinomlem  20055  gsumdixp  20135  prdsmgp  20136  prdsringd  20138  prdslmodd  20585  mulgrhm2  21054  frgpcyg  21135  evpmodpmf1o  21155  phlpropd  21214  frlmphl  21342  uvcresum  21354  frlmup1  21359  asclpropd  21457  psrass1lemOLD  21499  psrass1lem  21502  psrlinv  21522  psrass1  21531  psrdi  21532  psrdir  21533  psrass23l  21534  psrcom  21535  psrass23  21536  resspsrmul  21543  mplsubrglem  21569  mplmonmul  21597  mplcoe1  21598  mplcoe5  21601  mplcoe4  21638  evlslem3  21649  evlslem1  21651  mhpmulcl  21698  psrplusgpropd  21765  psropprmul  21767  coe1mul2  21798  coe1tm  21802  coe1tmmul2  21805  coe1tmmul  21806  coe1pwmul  21808  cply1mul  21825  ply1coe  21827  eqcoe1ply1eq  21828  lply1binomsc  21838  evl1gsummon  21891  mamures  21899  grpvrinv  21905  mhmvlin  21906  mamuass  21909  mamudi  21910  mamudir  21911  mamuvs1  21912  mamuvs2  21913  mpomatmul  21955  mamutpos  21967  madetsumid  21970  dmatmul  22006  scmatscm  22022  1mavmul  22057  mavmulass  22058  mvmumamul1  22063  mulmarep1gsum1  22082  mulmarep1gsum2  22083  mdetleib2  22097  mdetfval1  22099  mdet0pr  22101  mdetdiag  22108  mdetdiagid  22109  mdetrlin  22111  mdetrsca  22112  mdetralt  22117  mdetunilem9  22129  gsummatr01  22168  smadiadetlem1a  22172  smadiadetlem3  22177  smadiadetlem4  22178  cpmatmcllem  22227  mat2pmatmul  22240  decpmatmullem  22280  decpmatmul  22281  pmatcollpw1lem2  22284  pmatcollpw  22290  pmatcollpw3lem  22292  pmatcollpwscmat  22300  idpm2idmp  22310  mp2pm2mplem3  22317  mp2pm2mplem4  22318  mp2pm2mplem5  22319  mp2pm2mp  22320  pm2mpghm  22325  pm2mpmhmlem2  22328  monmat2matmon  22333  pm2mp  22334  chpdmat  22350  chpscmat  22351  chpscmatgsumbin  22353  chpscmatgsummon  22354  chp0mat  22355  chpidmat  22356  chfacfscmulgsum  22369  chfacfpmmulgsum  22373  chfacfpmmulgsum2  22374  cayhamlem1  22375  cpmidgsumm2pm  22378  cpmidpmat  22382  cpmadugsumlemB  22383  cpmadugsumlemC  22384  cpmadugsumlemF  22385  cpmadumatpoly  22392  cayhamlem3  22396  cayhamlem4  22397  cayleyhamilton0  22398  cayleyhamiltonALT  22400  neiptopnei  22643  neiptopreu  22644  ptcnplem  23132  cnmpt1t  23176  cnmpt12  23178  cnmptkp  23191  cnmptk1  23192  cnmpt1k  23193  cnmptkk  23194  cnmptk1p  23196  cnmpt2k  23199  qtopeu  23227  pt1hmeo  23317  ptunhmeo  23319  xkocnv  23325  xkohmeo  23326  flfcnp2  23518  cnmpt1plusg  23598  istgp2  23602  tmdmulg  23603  tgpmulg  23604  tmdgsum  23606  subgtgp  23616  symgtgp  23617  tgpconncomp  23624  prdstgpd  23636  tsmsmhm  23657  tsmsadd  23658  tsmssub  23660  tgptsmscls  23661  tsmssplit  23663  tsmsxplem1  23664  tsmsxplem2  23665  cnmpt1vsca  23705  tlmtgp  23707  ustuqtoplem  23751  utopsnneip  23760  ressprdsds  23884  metuval  24065  nmfval0  24106  tngnm  24175  nmoeq0  24260  idnghm  24267  cnmpt1ds  24365  fsumcn  24393  expcn  24395  divccn  24396  divccncf  24429  negcncf  24445  copco  24541  pcopt  24545  pcopt2  24546  pcoass  24547  pi1xfrcnvlem  24579  cnmpt1ip  24771  rrxnm  24915  rrxds  24917  minveclem3b  24952  divcncf  24971  ovolctb  25014  ovoliunnul  25031  voliunlem3  25076  ovolfs2  25095  uniioombllem2  25107  vitalilem4  25135  vitalilem5  25136  ismbf  25152  mbfss  25170  mbfmulc2re  25172  mbfneg  25174  mbfpos  25175  mbfposb  25177  mbfadd  25185  mbfsub  25186  mbfmulc2  25187  mbfinf  25189  mbflimsup  25190  mbflimlem  25191  i1fpos  25231  i1fposd  25232  itg1climres  25239  mbfmul  25251  itg2mulc  25272  itg2i1fseq  25280  itg2cnlem1  25286  itg2cnlem2  25287  itgresr  25303  iblneg  25327  i1fibl  25332  itgitg1  25333  iblsub  25346  itgfsum  25351  itgmulc2lem1  25356  limcmpt  25407  limccnp  25415  limcco  25417  dvreslem  25433  dvres2lem  25434  dvidlem  25439  dvcnp2  25444  dvaddbr  25462  dvmulbr  25463  dvmulf  25467  dvcmulf  25469  dvcobr  25470  dvcof  25472  dvcjbr  25473  dvcj  25474  dvfre  25475  dvexp  25477  dvexp2  25478  dvrec  25479  dvmptcmul  25488  dvmptdivc  25489  dvmptneg  25490  dvmptsub  25491  dvmptre  25493  dvmptim  25494  dvrecg  25497  dvmptdiv  25498  dvmptfsum  25499  dvcnvlem  25500  dvcnv  25501  dvexp3  25502  dvef  25504  dvsincos  25505  dv11cn  25525  lhop2  25539  lhop  25540  ftc2  25568  itgparts  25571  itgsubstlem  25572  mdegfval  25587  mdegmullem  25603  ply1termlem  25724  plypow  25726  plyconst  25727  plyeq0lem  25731  plypf1  25733  plyaddlem1  25734  plymullem1  25735  coeeulem  25745  coeidlem  25758  plyco  25762  coeeq2  25763  0dgr  25766  0dgrb  25767  dgrcolem1  25794  dgrcolem2  25795  plycjlem  25797  dvply1  25804  dvply2g  25805  plydiveu  25818  plyremlem  25824  elqaalem3  25841  taylfval  25878  dvtaylp  25889  taylthlem1  25892  taylthlem2  25893  ulmshft  25909  mtestbdd  25924  iblulm  25926  itgulm2  25928  pserulm  25941  psercn2  25942  pserdvlem2  25947  pserdv  25948  pserdv2  25949  abelthlem1  25950  abelthlem3  25952  advlog  26169  advlogexp  26170  dvcxp1  26255  dvcxp2  26256  dvcncxp1  26258  sqrtcn  26265  loglesqrt  26273  dvatan  26447  atantayl2  26450  atantayl3  26451  leibpi  26454  rlimcnp2  26478  efrlim  26481  dfef2  26482  cxp2lim  26488  divsqrtsumlem  26491  lgamgulmlem2  26541  lgamgulm2  26547  lgamcvglem  26551  gamcvg2lem  26570  ftalem7  26590  basellem9  26600  muinv  26704  logfacrlim  26734  logexprlim  26735  dchrmullid  26762  dchrinvcl  26763  lgseisenlem3  26887  lgseisenlem4  26888  chtppilimlem2  26984  chebbnd2  26987  chpchtlim  26989  chpo1ub  26990  rpvmasumlem  26997  dchrmusumlema  27003  dchrvmasumlem1  27005  dchrvmasumiflem2  27012  dchrisum0fno1  27021  rpvmasum2  27022  dchrisum0lema  27024  dchrisum0lem1  27026  dchrisum0lem2a  27027  dchrisum0lem2  27028  dchrisum0  27030  dchrmusumlem  27032  dchrvmasumlem  27033  rpvmasum  27036  rplogsum  27037  logdivsum  27043  mulog2sumlem3  27046  vmalogdivsum2  27048  vmalogdivsum  27049  2vmadivsumlem  27050  logsqvma2  27053  log2sumbnd  27054  selberglem2  27056  selberg3lem1  27067  selberg3  27069  selberg4lem1  27070  selberg4  27071  pntrsumo1  27075  selberg3r  27079  selberg4r  27080  selberg34r  27081  pntrlog2bndlem2  27088  pntrlog2bndlem4  27090  pntrlog2bndlem5  27091  pntrlog2bndlem6  27093  padicabvf  27141  padicabvcxp  27142  mirval  27944  crctcshlem4  29112  clwlknf1oclwwlkn  29375  eucrct2eupth  29536  chscllem4  30931  brafnmul  31242  kbmul  31246  cofmpt2  31896  ofresid  31905  ofoprabco  31927  fcobijfs  31986  gsummpt2d  32242  gsummptres  32245  gsummptres2  32246  gsumpart  32248  gsumhashmul  32249  fzto1st1  32302  fzto1st  32303  freshmansdream  32422  qusbas2  32562  qusima  32564  elrspunidl  32591  elrspunsn  32592  evls1fpws  32691  gsummoncoe1fzo  32714  lbsdiflsp0  32770  fedgmullem1  32773  fedgmullem2  32774  mdetpmtr1  32872  mdetlap  32881  xrge0mulc1cn  32990  esumval  33113  esumsnf  33131  esumpcvgval  33145  esumcvg  33153  esumcvgsum  33155  esumsup  33156  ofcfeqd2  33168  meascnbl  33286  sitgval  33400  probmeasb  33498  cndprobprob  33506  dstfrvclim1  33545  ballotlemfval  33557  ballotlemsval  33576  ballotlemieq  33584  plymul02  33626  plymulx0  33627  plymulx  33628  signsplypnf  33630  signstfv  33643  signstfvn  33649  signstfvp  33651  itgexpif  33687  logdivsqrle  33731  ptpconn  34293  cvmliftlem6  34350  cvmliftphtlem  34377  cvmlift3lem5  34383  elmrsubrn  34580  msubfval  34584  msubco  34591  divcnvlin  34771  gg-expcn  35233  gg-divccn  35234  gg-negcncf  35235  gg-dvcnp2  35243  gg-dvmulbr  35244  gg-dvcobr  35245  gg-psercn2  35247  knoppcnlem9  35463  knoppcnlem10  35464  knoppcnlem11  35465  bj-finsumval0  36252  curf  36552  matunitlindflem1  36570  matunitlindflem2  36571  poimirlem3  36577  poimirlem15  36589  poimirlem16  36590  poimirlem17  36591  poimirlem19  36593  poimirlem20  36594  broucube  36608  ovoliunnfl  36616  voliunnfl  36618  volsupnfl  36619  mbfposadd  36621  itg2addnclem  36625  itg2addnclem3  36627  itg2addnc  36628  itgaddnclem2  36633  itgaddnc  36634  iblsubnc  36635  itgsubnc  36636  itgmulc2nclem1  36640  itgmulc2nclem2  36641  itgmulc2nc  36642  itgabsnc  36643  ftc1cnnclem  36645  ftc1anclem3  36649  ftc1anclem5  36651  ftc1anclem6  36652  ftc1anclem8  36654  ftc1anc  36655  ftc2nc  36656  areacirclem1  36662  areacirclem2  36663  areacirclem4  36665  areacirc  36667  upixp  36683  lcmineqlem8  40987  lcmineqlem12  40991  dvrelog2b  41017  dvrelogpow2b  41019  aks4d1p1p6  41024  aks4d1p1p5  41026  sticksstones12a  41059  sticksstones12  41060  sticksstones19  41067  qsalrel  41148  pwsgprod  41196  rhmcomulmpl  41206  evlsvvval  41217  evlsevl  41225  selvvvval  41239  evlselv  41241  fsuppssindlem1  41245  fsuppssind  41247  mhphf  41251  mzpsubst  41568  mzprename  41569  mzpcompact2lem  41571  eldioph2  41582  rabdiophlem2  41622  mendlmod  42017  mendassa  42018  areaquad  42047  fsovcnvlem  42846  hashnzfzclim  43163  expgrowthi  43174  expgrowth  43176  uzmptshftfval  43187  dvradcnv2  43188  binomcxplemrat  43191  binomcxplemfrat  43192  binomcxplemradcnv  43193  binomcxplemdvbinom  43194  binomcxplemcvg  43195  binomcxplemdvsum  43196  binomcxplemnotnn0  43197  mulc1cncfg  44384  expcnfg  44386  fprodcnlem  44394  clim1fr1  44396  divcnvg  44422  sublimc  44447  reclimc  44448  divlimc  44451  limsupresico  44495  limsuppnfdlem  44496  limsupvaluz  44503  supcnvlimsupmpt  44536  liminfresico  44566  climliminflimsupd  44596  cncfmptssg  44666  negcncfg  44676  cncficcgt0  44683  fprodcncf  44695  fprodsubrecnncnvlem  44702  fprodaddrecnncnvlem  44704  dvsinax  44708  dvasinbx  44715  dvdivf  44717  ioodvbdlimc1lem2  44727  ioodvbdlimc2lem  44729  dvnmptdivc  44733  dvxpaek  44735  dvnxpaek  44737  dvnmul  44738  dvnprodlem2  44742  ibliccsinexp  44746  itgsinexplem1  44749  itgsinexp  44750  iblempty  44760  itgcoscmulx  44764  itgsincmulx  44769  itgioocnicc  44772  iblcncfioo  44773  itgsbtaddcnst  44777  volioofmpt  44789  volicofmpt  44792  stoweidlem4  44799  stirlinglem5  44873  dirkerval  44886  dirkertrigeq  44896  dirkeritg  44897  dirkercncflem2  44899  dirkercncflem4  44901  fourierdlem16  44918  fourierdlem18  44920  fourierdlem21  44923  fourierdlem22  44924  fourierdlem28  44930  fourierdlem39  44941  fourierdlem40  44942  fourierdlem41  44943  fourierdlem53  44954  fourierdlem56  44957  fourierdlem57  44958  fourierdlem60  44961  fourierdlem61  44962  fourierdlem68  44969  fourierdlem73  44974  fourierdlem74  44975  fourierdlem75  44976  fourierdlem76  44977  fourierdlem78  44979  fourierdlem81  44982  fourierdlem82  44983  fourierdlem83  44984  fourierdlem84  44985  fourierdlem85  44986  fourierdlem88  44989  fourierdlem90  44991  fourierdlem92  44993  fourierdlem93  44994  fourierdlem95  44996  fourierdlem97  44998  fourierdlem101  45002  fourierdlem103  45004  fourierdlem104  45005  fourierdlem111  45012  fourierdlem112  45013  sqwvfoura  45023  sqwvfourb  45024  fouriersw  45026  elaa2lem  45028  etransclem4  45033  etransclem17  45046  etransclem18  45047  etransclem32  45061  etransclem46  45075  sge0z  45170  sge0revalmpt  45173  sge0tsms  45175  sge0sup  45186  sge0iunmptlemre  45210  sge0iun  45214  sge0xaddlem2  45229  ismeannd  45262  psmeasurelem  45265  meaiuninclem  45275  meaiininclem  45281  caratheodory  45323  isomenndlem  45325  ovnval  45336  hoicvrrex  45351  ovnlecvr  45353  ovncvrrp  45359  ovn0lem  45360  ovnsubaddlem1  45365  hoidmv1lelem2  45387  hoidmv1le  45389  hoidmvlelem3  45392  ovnhoilem2  45397  ovnhoi  45398  ovnlecvr2  45405  ovncvr2  45406  hspmbllem2  45422  ovolval2lem  45438  ovolval3  45442  ovolval5lem1  45447  ovolval5lem2  45448  ovnovollem1  45451  ovnovollem2  45452  vonioolem1  45475  vonicclem1  45478  vonct  45488  smflim  45572  smfinflem  45612  smflimsuplem5  45619  smfliminflem  45625  cfsetsnfsetfv  45846  fundcmpsurbijinjpreimafv  46154  fundcmpsurinjimaid  46158  prdsrngd  46756  fdmdifeqresdif  47096  ply1mulgsumlem2  47146  lincvalsc0  47180  linc0scn0  47182  lincdifsn  47183  lincsum  47188  lincscm  47189  lindslinindimp2lem4  47220  lindslinindsimp2lem5  47221  lincresunit3lem2  47239  1arymaptfo  47407  itcovalpclem1  47434  itcovalpclem2  47435  itcovalt2lem1  47439  itcovalt2lem2  47440  aacllem  47926  amgmwlem  47927