Theorem mpteq2dva 5185

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 2730	. 2 ⊢ (𝜑 → 𝐴 = 𝐴)
2		mpteq2dva.1	. 2 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 = 𝐶)
3	1, 2	mpteq12dva 5178	1 ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵) = (𝑥 ∈ 𝐴 ↦ 𝐶))

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

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 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-opab 5155  df-mpt 5174

This theorem is referenced by:  mpteq2dv  5186  mpteq2ia  5187  2fvcoidd  7234  offval  7622  offval2  7633  coof  7637  caofinvl  7645  caofcom  7650  caofass  7653  caofdi  7655  caofdir  7656  caonncan  7657  curry1  8037  curry2  8040  mpocurryd  8202  pw2f1olem  8998  mapxpen  9060  xpmapenlem  9061  cantnfp1  9577  cantnflem1d  9584  cantnflem1  9585  cnfcom2lem  9597  dfac12lem1  10038  seqof  13966  seqof2  13967  swrdswrd  14611  repswswrd  14690  repswrevw  14693  revco  14741  ccatco  14742  repsco  14747  ofccat  14876  lo1eq  15475  rlimeq  15476  lo1mul2  15536  o1dif  15537  lo1sub  15538  rlimdiv  15553  caucvgr  15583  sumeq1  15596  fsumrlim  15718  fsumo1  15719  climfsum  15727  geomulcvg  15783  vdwlem8  16900  prmgapprmo  16974  restid2  17334  pwsplusgval  17394  pwsmulrval  17395  pwsvscafval  17398  qusin  17448  xpsaddlem  17477  xpsvsca  17481  catidd  17586  fuclid  17876  fucrid  17877  fucass  17878  setcepi  17995  prf1st  18110  prf2nd  18111  1st2ndprf  18112  curfcl  18138  curfuncf  18144  diag2  18151  curf2ndf  18153  hof2val  18162  hofcllem  18164  hofcl  18165  yonedalem4a  18181  yonedalem4c  18183  yonedalem3b  18185  yonedainv  18187  yonffthlem  18188  prdssgrpd  18607  prdsidlem  18643  prdsmndd  18644  mhmvlin  18675  pwsco2mhm  18707  frmdup3lem  18740  frmdup3  18741  smndex1gid  18777  smndex1igid  18778  grpinvpropd  18894  prdsinvlem  18928  pwsinvg  18932  pwssub  18933  galactghm  19283  cayleylem1  19291  pmtrprfval  19366  sylow1lem2  19478  sylow3lem1  19506  efginvrel1  19607  frgpup3lem  19656  frgpup3  19657  prdscmnd  19740  iscyggen  19759  gsumval3  19786  gsumcllem  19787  gsumzsplit  19806  gsumsub  19827  gsummptf1o  19842  gsum2d  19851  gsum2d2  19853  gsumxp  19855  prdsgsum  19860  telgsumfz  19869  telgsumfz0  19871  telgsum  19873  dprdfsub  19902  dprdfeq0  19903  dprddisj2  19920  dprd2d2  19925  dpjidcl  19939  ablfaclem2  19967  ablfac2  19970  prdsmgp  20036  prdsrngd  20061  srgbinomlem3  20113  srgbinomlem4  20114  srgbinomlem  20115  gsumdixp  20204  prdsringd  20206  prdslmodd  20872  mulgrhm2  21385  frgpcyg  21480  freshmansdream  21481  evpmodpmf1o  21503  phlpropd  21562  frlmphl  21688  uvcresum  21700  frlmup1  21705  asclpropd  21804  psrass1lem  21839  psrlinv  21862  psrass1  21871  psrdi  21872  psrdir  21873  psrass23l  21874  psrcom  21875  psrass23  21876  resspsrmul  21883  mplsubrglem  21911  mplmonmul  21941  mplcoe1  21942  mplcoe5  21945  mplcoe4  21976  evlslem3  21985  evlslem1  21987  mhpmulcl  22034  psdmplcl  22047  psdadd  22048  psdmul  22051  psdmvr  22054  psrplusgpropd  22118  psropprmul  22120  coe1mul2  22153  coe1tm  22157  coe1tmmul2  22160  coe1tmmul  22161  coe1pwmul  22163  cply1mul  22181  ply1coe  22183  eqcoe1ply1eq  22184  lply1binomsc  22196  evl1gsummon  22250  evls1fpws  22254  rhmcomulmpl  22267  mamures  22282  grpvrinv  22284  mamuass  22287  mamudi  22288  mamudir  22289  mamuvs1  22290  mamuvs2  22291  mpomatmul  22331  mamutpos  22343  madetsumid  22346  dmatmul  22382  scmatscm  22398  1mavmul  22433  mavmulass  22434  mvmumamul1  22439  mulmarep1gsum1  22458  mulmarep1gsum2  22459  mdetleib2  22473  mdetfval1  22475  mdet0pr  22477  mdetdiag  22484  mdetdiagid  22485  mdetrlin  22487  mdetrsca  22488  mdetralt  22493  mdetunilem9  22505  gsummatr01  22544  smadiadetlem1a  22548  smadiadetlem3  22553  smadiadetlem4  22554  cpmatmcllem  22603  mat2pmatmul  22616  decpmatmullem  22656  decpmatmul  22657  pmatcollpw1lem2  22660  pmatcollpw  22666  pmatcollpw3lem  22668  pmatcollpwscmat  22676  idpm2idmp  22686  mp2pm2mplem3  22693  mp2pm2mplem4  22694  mp2pm2mplem5  22695  mp2pm2mp  22696  pm2mpghm  22701  pm2mpmhmlem2  22704  monmat2matmon  22709  pm2mp  22710  chpdmat  22726  chpscmat  22727  chpscmatgsumbin  22729  chpscmatgsummon  22730  chp0mat  22731  chpidmat  22732  chfacfscmulgsum  22745  chfacfpmmulgsum  22749  chfacfpmmulgsum2  22750  cayhamlem1  22751  cpmidgsumm2pm  22754  cpmidpmat  22758  cpmadugsumlemB  22759  cpmadugsumlemC  22760  cpmadugsumlemF  22761  cpmadumatpoly  22768  cayhamlem3  22772  cayhamlem4  22773  cayleyhamilton0  22774  cayleyhamiltonALT  22776  neiptopnei  23017  neiptopreu  23018  ptcnplem  23506  cnmpt1t  23550  cnmpt12  23552  cnmptkp  23565  cnmptk1  23566  cnmpt1k  23567  cnmptkk  23568  cnmptk1p  23570  cnmpt2k  23573  qtopeu  23601  pt1hmeo  23691  ptunhmeo  23693  xkocnv  23699  xkohmeo  23700  flfcnp2  23892  cnmpt1plusg  23972  istgp2  23976  tmdmulg  23977  tgpmulg  23978  tmdgsum  23980  subgtgp  23990  symgtgp  23991  tgpconncomp  23998  prdstgpd  24010  tsmsmhm  24031  tsmsadd  24032  tsmssub  24034  tgptsmscls  24035  tsmssplit  24037  tsmsxplem1  24038  tsmsxplem2  24039  cnmpt1vsca  24079  tlmtgp  24081  ustuqtoplem  24125  utopsnneip  24134  ressprdsds  24257  metuval  24435  nmfval0  24476  tngnm  24537  nmoeq0  24622  idnghm  24629  cnmpt1ds  24729  fsumcn  24759  expcn  24761  divccn  24762  expcnOLD  24763  divccnOLD  24764  divccncf  24797  negcncf  24813  negcncfOLD  24814  copco  24916  pcopt  24920  pcopt2  24921  pcoass  24922  pi1xfrcnvlem  24954  cnmpt1ip  25145  rrxnm  25289  rrxds  25291  minveclem3b  25326  divcncf  25346  ovolctb  25389  ovoliunnul  25406  voliunlem3  25451  ovolfs2  25470  uniioombllem2  25482  vitalilem4  25510  vitalilem5  25511  ismbf  25527  mbfss  25545  mbfmulc2re  25547  mbfneg  25549  mbfpos  25550  mbfposb  25552  mbfadd  25560  mbfsub  25561  mbfmulc2  25562  mbfinf  25564  mbflimsup  25565  mbflimlem  25566  i1fpos  25605  i1fposd  25606  itg1climres  25613  mbfmul  25625  itg2mulc  25646  itg2i1fseq  25654  itg2cnlem1  25660  itg2cnlem2  25661  itgresr  25678  iblneg  25702  i1fibl  25707  itgitg1  25708  iblsub  25721  itgfsum  25726  itgmulc2lem1  25731  limcmpt  25782  limccnp  25790  limcco  25792  dvreslem  25808  dvres2lem  25809  dvidlem  25814  dvcnp2  25819  dvcnp2OLD  25820  dvaddbr  25838  dvmulbr  25839  dvmulbrOLD  25840  dvmulf  25844  dvcmulf  25846  dvcobr  25847  dvcobrOLD  25848  dvcof  25850  dvcjbr  25851  dvcj  25852  dvfre  25853  dvexp  25855  dvexp2  25856  dvrec  25857  dvmptcmul  25866  dvmptdivc  25867  dvmptneg  25868  dvmptsub  25869  dvmptre  25871  dvmptim  25872  dvrecg  25875  dvmptdiv  25876  dvmptfsum  25877  dvcnvlem  25878  dvcnv  25879  dvexp3  25880  dvef  25882  dvsincos  25883  dv11cn  25904  lhop2  25918  lhop  25919  ftc2  25949  itgparts  25952  itgsubstlem  25953  mdegfval  25965  mdegmullem  25981  ply1termlem  26106  plypow  26108  plyconst  26109  plyeq0lem  26113  plypf1  26115  plyaddlem1  26116  plymullem1  26117  coeeulem  26127  coeidlem  26140  plyco  26144  coeeq2  26145  0dgr  26148  0dgrb  26149  dgrcolem1  26177  dgrcolem2  26178  plycjlem  26180  dvply1  26189  dvply2g  26190  dvply2gOLD  26191  plydiveu  26204  plyremlem  26210  elqaalem3  26227  taylfval  26264  dvtaylp  26276  taylthlem1  26279  taylthlem2  26280  taylthlem2OLD  26281  ulmshft  26297  mtestbdd  26312  iblulm  26314  itgulm2  26316  pserulm  26329  psercn2  26330  psercn2OLD  26331  pserdvlem2  26336  pserdv  26337  pserdv2  26338  abelthlem1  26339  abelthlem3  26341  advlog  26561  advlogexp  26562  dvcxp1  26647  dvcxp2  26648  dvcncxp1  26650  sqrtcn  26658  loglesqrt  26669  dvatan  26843  atantayl2  26846  atantayl3  26847  leibpi  26850  rlimcnp2  26874  efrlim  26877  efrlimOLD  26878  dfef2  26879  cxp2lim  26885  divsqrtsumlem  26888  lgamgulmlem2  26938  lgamgulm2  26944  lgamcvglem  26948  gamcvg2lem  26967  ftalem7  26987  basellem9  26997  muinv  27101  logfacrlim  27133  logexprlim  27134  dchrmullid  27161  dchrinvcl  27162  lgseisenlem3  27286  lgseisenlem4  27287  chtppilimlem2  27383  chebbnd2  27386  chpchtlim  27388  chpo1ub  27389  rpvmasumlem  27396  dchrmusumlema  27402  dchrvmasumlem1  27404  dchrvmasumiflem2  27411  dchrisum0fno1  27420  rpvmasum2  27421  dchrisum0lema  27423  dchrisum0lem1  27425  dchrisum0lem2a  27426  dchrisum0lem2  27427  dchrisum0  27429  dchrmusumlem  27431  dchrvmasumlem  27432  rpvmasum  27435  rplogsum  27436  logdivsum  27442  mulog2sumlem3  27445  vmalogdivsum2  27447  vmalogdivsum  27448  2vmadivsumlem  27449  logsqvma2  27452  log2sumbnd  27453  selberglem2  27455  selberg3lem1  27466  selberg3  27468  selberg4lem1  27469  selberg4  27470  pntrsumo1  27474  selberg3r  27478  selberg4r  27479  selberg34r  27480  pntrlog2bndlem2  27487  pntrlog2bndlem4  27489  pntrlog2bndlem5  27490  pntrlog2bndlem6  27492  padicabvf  27540  padicabvcxp  27541  mirval  28600  crctcshlem4  29765  clwlknf1oclwwlkn  30028  eucrct2eupth  30189  chscllem4  31584  brafnmul  31895  kbmul  31899  cofmpt2  32578  ofresid  32586  ofoprabco  32608  fmptunsnop  32643  fcobijfs  32666  fcobijfs2  32667  gsummpt2d  33003  gsummptres  33006  gsummptres2  33007  gsummptfsf1o  33008  gsumfs2d  33009  gsumpart  33011  gsumhashmul  33015  gsumwrd2dccat  33021  fzto1st1  33045  fzto1st  33046  elrgspnlem1  33183  elrgspnlem2  33184  elrgspnlem3  33185  elrgspnlem4  33186  elrgspnsubrunlem1  33188  elrgspnsubrunlem2  33189  qusbas2  33344  qusima  33346  elrspunidl  33366  elrspunsn  33367  rprmdvdsprod  33472  ressply1evls1  33501  evl1deg1  33512  evl1deg2  33513  evl1deg3  33514  gsummoncoe1fzo  33531  mplvrpmga  33548  mplvrpmmhm  33549  lbsdiflsp0  33599  fedgmullem1  33602  fedgmullem2  33603  fldextrspunlsplem  33646  fldextrspunlsp  33647  extdgfialglem2  33666  mdetpmtr1  33796  mdetlap  33805  xrge0mulc1cn  33914  esumval  34019  esumsnf  34037  esumpcvgval  34051  esumcvg  34059  esumcvgsum  34061  esumsup  34062  ofcfeqd2  34074  meascnbl  34192  sitgval  34306  probmeasb  34404  cndprobprob  34412  dstfrvclim1  34452  ballotlemfval  34464  ballotlemsval  34483  ballotlemieq  34491  plymul02  34520  plymulx0  34521  plymulx  34522  signsplypnf  34524  signstfv  34537  signstfvn  34543  signstfvp  34545  itgexpif  34580  logdivsqrle  34624  ptpconn  35216  cvmliftlem6  35273  cvmliftphtlem  35300  cvmlift3lem5  35306  elmrsubrn  35503  msubfval  35507  msubco  35514  divcnvlin  35716  knoppcnlem9  36485  knoppcnlem10  36486  knoppcnlem11  36487  bj-finsumval0  37269  curf  37588  matunitlindflem1  37606  matunitlindflem2  37607  poimirlem3  37613  poimirlem15  37625  poimirlem16  37626  poimirlem17  37627  poimirlem19  37629  poimirlem20  37630  broucube  37644  ovoliunnfl  37652  voliunnfl  37654  volsupnfl  37655  mbfposadd  37657  itg2addnclem  37661  itg2addnclem3  37663  itg2addnc  37664  itgaddnclem2  37669  itgaddnc  37670  iblsubnc  37671  itgsubnc  37672  itgmulc2nclem1  37676  itgmulc2nclem2  37677  itgmulc2nc  37678  itgabsnc  37679  ftc1cnnclem  37681  ftc1anclem3  37685  ftc1anclem5  37687  ftc1anclem6  37688  ftc1anclem8  37690  ftc1anc  37691  ftc2nc  37692  areacirclem1  37698  areacirclem2  37699  areacirclem4  37701  areacirc  37703  upixp  37719  lcmineqlem8  42019  lcmineqlem12  42023  dvrelog2b  42049  dvrelogpow2b  42051  aks4d1p1p6  42056  aks4d1p1p5  42058  aks6d1c1  42099  aks6d1c5lem3  42120  sticksstones12a  42140  sticksstones12  42141  sticksstones19  42148  aks6d1c6lem1  42153  aks6d1c6lem4  42156  aks6d1c7lem3  42165  qsalrel  42223  pwsgprod  42527  rhmcomulpsr  42534  evlsvvval  42546  evlsevl  42554  selvvvval  42568  evlselv  42570  fsuppssindlem1  42574  fsuppssind  42576  mhphf  42580  mzpsubst  42731  mzprename  42732  mzpcompact2lem  42734  eldioph2  42745  rabdiophlem2  42785  mendlmod  43172  mendassa  43173  areaquad  43199  fsovcnvlem  43996  hashnzfzclim  44305  expgrowthi  44316  expgrowth  44318  uzmptshftfval  44329  dvradcnv2  44330  binomcxplemrat  44333  binomcxplemfrat  44334  binomcxplemradcnv  44335  binomcxplemdvbinom  44336  binomcxplemcvg  44337  binomcxplemdvsum  44338  binomcxplemnotnn0  44339  mulc1cncfg  45580  expcnfg  45582  fprodcnlem  45590  clim1fr1  45592  divcnvg  45618  sublimc  45643  reclimc  45644  divlimc  45647  limsupresico  45691  limsuppnfdlem  45692  limsupvaluz  45699  supcnvlimsupmpt  45732  liminfresico  45762  climliminflimsupd  45792  cncfmptssg  45862  negcncfg  45872  cncficcgt0  45879  fprodcncf  45891  fprodsubrecnncnvlem  45898  fprodaddrecnncnvlem  45900  dvsinax  45904  dvasinbx  45911  dvdivf  45913  ioodvbdlimc1lem2  45923  ioodvbdlimc2lem  45925  dvnmptdivc  45929  dvxpaek  45931  dvnxpaek  45933  dvnmul  45934  dvnprodlem2  45938  ibliccsinexp  45942  itgsinexplem1  45945  itgsinexp  45946  iblempty  45956  itgcoscmulx  45960  itgsincmulx  45965  itgioocnicc  45968  iblcncfioo  45969  itgsbtaddcnst  45973  volioofmpt  45985  volicofmpt  45988  stoweidlem4  45995  stirlinglem5  46069  dirkerval  46082  dirkertrigeq  46092  dirkeritg  46093  dirkercncflem2  46095  dirkercncflem4  46097  fourierdlem16  46114  fourierdlem18  46116  fourierdlem21  46119  fourierdlem22  46120  fourierdlem28  46126  fourierdlem39  46137  fourierdlem40  46138  fourierdlem41  46139  fourierdlem53  46150  fourierdlem56  46153  fourierdlem57  46154  fourierdlem60  46157  fourierdlem61  46158  fourierdlem68  46165  fourierdlem73  46170  fourierdlem74  46171  fourierdlem75  46172  fourierdlem76  46173  fourierdlem78  46175  fourierdlem81  46178  fourierdlem82  46179  fourierdlem83  46180  fourierdlem84  46181  fourierdlem85  46182  fourierdlem88  46185  fourierdlem90  46187  fourierdlem92  46189  fourierdlem93  46190  fourierdlem95  46192  fourierdlem97  46194  fourierdlem101  46198  fourierdlem103  46200  fourierdlem104  46201  fourierdlem111  46208  fourierdlem112  46209  sqwvfoura  46219  sqwvfourb  46220  fouriersw  46222  elaa2lem  46224  etransclem4  46229  etransclem17  46242  etransclem18  46243  etransclem32  46257  etransclem46  46271  sge0z  46366  sge0revalmpt  46369  sge0tsms  46371  sge0sup  46382  sge0iunmptlemre  46406  sge0iun  46410  sge0xaddlem2  46425  ismeannd  46458  psmeasurelem  46461  meaiuninclem  46471  meaiininclem  46477  caratheodory  46519  isomenndlem  46521  ovnval  46532  hoicvrrex  46547  ovnlecvr  46549  ovncvrrp  46555  ovn0lem  46556  ovnsubaddlem1  46561  hoidmv1lelem2  46583  hoidmv1le  46585  hoidmvlelem3  46588  ovnhoilem2  46593  ovnhoi  46594  ovnlecvr2  46601  ovncvr2  46602  hspmbllem2  46618  ovolval2lem  46634  ovolval3  46638  ovolval5lem1  46643  ovolval5lem2  46644  ovnovollem1  46647  ovnovollem2  46648  vonioolem1  46671  vonicclem1  46674  vonct  46684  smflim  46768  smfinflem  46808  smflimsuplem5  46815  smfliminflem  46821  cfsetsnfsetfv  47051  fundcmpsurbijinjpreimafv  47401  fundcmpsurinjimaid  47405  fdmdifeqresdif  48336  ply1mulgsumlem2  48382  lincvalsc0  48416  linc0scn0  48418  lincdifsn  48419  lincsum  48424  lincscm  48425  lindslinindimp2lem4  48456  lindslinindsimp2lem5  48457  lincresunit3lem2  48475  1arymaptfo  48638  itcovalpclem1  48665  itcovalpclem2  48666  itcovalt2lem1  48670  itcovalt2lem2  48671  tposcurf1  49294  tposcurf2  49295  diag1  49299  fuco22  49334  fucocolem2  49349  fucocolem3  49350  fucocolem4  49351  fucoco  49352  fucolid  49356  fucorid  49357  postcofval  49359  precofval  49362  precofvalALT  49363  precofval2  49364  fucoppcco  49404  islmd  49660  iscmd  49661  aacllem  49796  amgmwlem  49797