Theorem mpteq2ia 4534

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 2457	. . 3
2	1	ax-gen 1618	. 2
3		mpteq2ia.1	. . 3
4	3	rgen 2817	. 2
5		mpteq12f 4528	. 2
6	2, 4, 5	mp2an 672	1

Syntax hints:  ->wi 4  A.wal 1393  =wceq 1395  e.wcel 1818  A.wral 2807  e.cmpt 4510

This theorem is referenced by:  mpteq2i  4535  feqresmpt  5927  elfvmptrab  5977  fmptap  6094  offres  6795  resixpfo  7527  dfoi  7957  cantnflem1d  8128  cantnflem1  8129  cantnflem1dOLD  8151  cantnflem1OLD  8152  dfceil2  11968  cnrecnv  12998  ackbijnn  13640  harmonic  13670  ege2le3  13825  eirrlem  13937  prmrec  14440  imasdsval2  14913  cayleylem1  16437  pmtrprfval  16512  gsumzsplit  16944  gsumzsplitOLD  16945  gsum2dlem2  16998  gsum2dOLD  17000  dmdprdsplitlem  17084  dmdprdsplitlemOLD  17085  coe1sclmul  18323  coe1sclmul2  18325  frlmip  18809  mdetunilem9  19122  leordtvallem1  19711  leordtvallem2  19712  txkgen  20153  cnmpt1st  20169  cnmpt2nd  20170  tmdgsum  20594  tsmssplit  20654  cnfldnm  21286  expcn  21376  pcorev2  21528  pi1xfrcnv  21557  rrxip  21822  mbfi1flim  22130  itg2uba  22150  itg2cnlem1  22168  itg2cnlem2  22169  itgitg2  22213  itgss3  22221  itgless  22223  ibladdlem  22226  itgaddlem1  22229  iblabslem  22234  itggt0  22248  itgcn  22249  limcdif  22280  limcres  22290  cnplimc  22291  dvcobr  22349  dvexp  22356  dveflem  22380  dvef  22381  dvlip  22394  dvlipcn  22395  lhop  22417  tdeglem2  22459  mdegfvalOLD  22461  plyid  22606  coeidp  22660  dgrid  22661  pserdvlem2  22823  abelth  22836  dvrelog  23018  logcn  23028  dvlog  23032  advlog  23035  advlogexp  23036  logtayl  23041  logccv  23044  dvcxp1  23116  dvsqrt  23118  resqrtcn  23123  loglesqrt  23132  dvatan  23266  leibpilem2  23272  leibpi  23273  efrlim  23299  sqrtlim  23302  amgmlem  23319  emcllem5  23329  chtublem  23486  logfacrlim2  23501  bposlem6  23564  chto1lb  23663  vmadivsum  23667  dchrvmasumlema  23685  mulogsumlem  23716  logdivsum  23718  logsqvma2  23728  log2sumbnd  23729  selberglem1  23730  selberglem3  23732  selberg  23733  selberg2lem  23735  selberg2  23736  pntrmax  23749  pntrsumo1  23750  selbergr  23753  selbergs  23759  pnt2  23798  pnt  23799  ostth2  23822  ostth  23824  hilnormi  26080  bra0  26869  partfun  27516  zrhre  27997  qqhre  27998  eulerpartgbij  28311  plymulx  28505  lgamgulmlem2  28572  lgam1  28606  faclim  29171  ptrest  30048  ovoliunnfl  30056  voliunnfl  30058  mbfposadd  30062  dvtan  30065  itg2addnclem  30066  ibladdnclem  30071  itgaddnclem1  30073  iblabsnclem  30078  itggt0cn  30087  ftc1anclem4  30093  ftc1anclem5  30094  ftc1anclem6  30095  ftc1anclem7  30096  ftc1anclem8  30097  dvcncxp1  30100  dvcnsqrt  30101  dvasin  30103  dvacos  30104  areacirclem1  30107  arearect  31183  areaquad  31184  lhe4.4ex1a  31234  binomcxplemrat  31255  dvnprodlem1  31743  itgsin0pilem1  31748  wallispilem4  31850  wallispi2  31855  stirlinglem1  31856  stirlinglem3  31858  dirkercncflem2  31886  fourierdlem48  31937  fourierdlem49  31938  fourierdlem56  31945  fourierdlem57  31946  fourierdlem58  31947  fourierdlem62  31951  fourierdlem107  31996  fouriersw  32014  etransclem46  32063

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-10 1837  ax-11 1842  ax-12 1854  ax-13 1999  ax-ext 2435

This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1398  df-ex 1613  df-nf 1617  df-sb 1740  df-clab 2443  df-cleq 2449  df-clel 2452  df-ral 2812  df-opab 4511  df-mpt 4512