Theorem mpteq2ia 4384

Description: An equality inference for the maps to notation. (Contributed by Mario Carneiro, 16-Dec-2013.)

Hypothesis

Ref	Expression
mpteq2ia.1

Assertion

Ref	Expression
mpteq2ia

Proof of Theorem mpteq2ia

Step	Hyp	Ref	Expression
1		eqid 2481	. . 3
2	1	ax-gen 1562	. 2
3		mpteq2ia.1	. . 3
4	3	rgen 2817	. 2
5		mpteq12f 4378	. 2
6	2, 4, 5	mp2an 655	1

Syntax hints:  ->wi 4  A.wal 1556  =wceq 1662  e.wcel 1724  A.wral 2751  e.cmpt 4360

This theorem is referenced by:  mpteq2i  4385  feqresmpt  5738  fmptap  5886  offres  6533  resixpfo  7212  dfoi  7592  cantnflem1d  7756  cantnflem1  7757  dfceil2  11472  cnrecnv  12440  ackbijnn  13077  harmonic  13107  ege2le3  13161  eirrlem  13272  prmrec  13769  imasdsval2  14233  cayleylem1  15613  gsumzsplit  16032  gsumsn  16046  gsum2d  16049  dmdprdsplitlem  16098  coe1sclmul  17177  coe1sclmul2  17179  leordtvallem1  17777  leordtvallem2  17778  txkgen  18188  cnmpt1st  18204  cnmpt2nd  18205  tmdgsum  18629  tsmssplit  18685  cnfldnm  19317  expcn  19406  pcorev2  19557  pi1xfrcnv  19586  mbfi1flim  20117  itg2uba  20137  itg2cnlem1  20155  itg2cnlem2  20156  itgitg2  20200  itgss3  20208  itgless  20210  ibladdlem  20213  itgaddlem1  20216  iblabslem  20221  itggt0  20235  itgcn  20236  limcdif  20267  limcres  20277  cnplimc  20278  dvcobr  20336  dvexp  20343  dveflem  20367  dvef  20368  dvlip  20381  dvlipcn  20382  lhop  20404  tdeglem2  20488  plyid  20632  coeidp  20685  dgrid  20686  pserdvlem2  20848  abelth  20861  dvrelog  21037  logcn  21047  dvlog  21051  advlog  21054  advlogexp  21055  logtayl  21060  logccv  21063  dvcxp1  21135  dvsqr  21137  resqrcn  21142  loglesqr  21151  dvatan  21284  leibpilem2  21290  leibpi  21291  efrlim  21317  sqrlim  21320  amgmlem  21337  emcllem5  21347  chtublem  21504  logfacrlim2  21519  bposlem6  21582  chto1lb  21681  vmadivsum  21685  dchrvmasumlema  21703  mulogsumlem  21734  logdivsum  21736  logsqvma2  21746  log2sumbnd  21747  selberglem1  21748  selberglem3  21750  selberg  21751  selberg2lem  21753  selberg2  21754  pntrmax  21767  pntrsumo1  21768  selbergr  21771  selbergs  21777  pnt2  21816  pnt  21817  ostth2  21840  ostth  21842  hilnormi  23175  bra0  23964  partfun  24614  gsumsnf  24895  zrhre  25116  qqhre  25117  eulerpartgbij  25420  plymulx  25591  lgamgulmlem2  25653  lgam1  25687  faclim  26195  ovoliunnfl  27104  voliunnfl  27106  mbfposadd  27110  dvtan  27113  itg2addnclem  27114  ibladdnclem  27119  itgaddnclem1  27121  iblabsnclem  27126  itggt0cn  27135  ftc1anclem4  27141  ftc1anclem5  27142  ftc1anclem6  27143  ftc1anclem7  27144  ftc1anclem8  27145  dvcncxp1  27148  dvcnsqr  27149  dvasin  27151  dvacos  27152  areacirclem1  27155  lhe4.4ex1a  28452  itgsin0pilem1  28644  wallispilem4  28717  wallispi2  28722  stirlinglem1  28723  stirlinglem3  28725  elfvmptrab  29014  pmtrprfval  29601

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1562  ax-4 1573  ax-5 1636  ax-6 1677  ax-7 1697  ax-10 1743  ax-11 1748  ax-12 1760  ax-13 1947  ax-ext 2462

This theorem depends on definitions:  df-bi 179  df-an 362  df-tru 1337  df-ex 1558  df-nf 1561  df-sb 1669  df-clab 2468  df-cleq 2474  df-clel 2477  df-ral 2756  df-opab 4361  df-mpt 4362