Theorem mpteq2ia 4491

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 2454	. . 3
2	1	ax-gen 1592	. 2
3		mpteq2ia.1	. . 3
4	3	rgen 2901	. 2
5		mpteq12f 4485	. 2
6	2, 4, 5	mp2an 672	1

Syntax hints:  ->wi 4  A.wal 1368  =wceq 1370  e.wcel 1758  A.wral 2800  e.cmpt 4467

This theorem is referenced by:  mpteq2i  4492  feqresmpt  5868  fmptap  6026  offres  6705  resixpfo  7435  dfoi  7862  cantnflem1d  8033  cantnflem1  8034  cantnflem1dOLD  8056  cantnflem1OLD  8057  dfceil2  11825  cnrecnv  12812  ackbijnn  13449  harmonic  13479  ege2le3  13533  eirrlem  13644  prmrec  14141  imasdsval2  14613  cayleylem1  16076  pmtrprfval  16152  gsumzsplit  16579  gsumzsplitOLD  16580  gsum2dlem2  16631  gsum2dOLD  16633  dmdprdsplitlem  16709  dmdprdsplitlemOLD  16710  coe1sclmul  17917  coe1sclmul2  17919  frlmip  18396  mdetunilem9  18694  leordtvallem1  19213  leordtvallem2  19214  txkgen  19624  cnmpt1st  19640  cnmpt2nd  19641  tmdgsum  20065  tsmssplit  20125  cnfldnm  20757  expcn  20847  pcorev2  20999  pi1xfrcnv  21028  rrxip  21293  mbfi1flim  21601  itg2uba  21621  itg2cnlem1  21639  itg2cnlem2  21640  itgitg2  21684  itgss3  21692  itgless  21694  ibladdlem  21697  itgaddlem1  21700  iblabslem  21705  itggt0  21719  itgcn  21720  limcdif  21751  limcres  21761  cnplimc  21762  dvcobr  21820  dvexp  21827  dveflem  21851  dvef  21852  dvlip  21865  dvlipcn  21866  lhop  21888  tdeglem2  21930  mdegfvalOLD  21932  plyid  22077  coeidp  22130  dgrid  22131  pserdvlem2  22293  abelth  22306  dvrelog  22482  logcn  22492  dvlog  22496  advlog  22499  advlogexp  22500  logtayl  22505  logccv  22508  dvcxp1  22580  dvsqr  22582  resqrcn  22587  loglesqr  22596  dvatan  22730  leibpilem2  22736  leibpi  22737  efrlim  22763  sqrlim  22766  amgmlem  22783  emcllem5  22793  chtublem  22950  logfacrlim2  22965  bposlem6  23028  chto1lb  23127  vmadivsum  23131  dchrvmasumlema  23149  mulogsumlem  23180  logdivsum  23182  logsqvma2  23192  log2sumbnd  23193  selberglem1  23194  selberglem3  23196  selberg  23197  selberg2lem  23199  selberg2  23200  pntrmax  23213  pntrsumo1  23214  selbergr  23217  selbergs  23223  pnt2  23262  pnt  23263  ostth2  23286  ostth  23288  hilnormi  25034  bra0  25823  partfun  26460  zrhre  26902  qqhre  26903  eulerpartgbij  27211  plymulx  27405  lgamgulmlem2  27472  lgam1  27506  faclim  28008  ptrest  28885  ovoliunnfl  28893  voliunnfl  28895  mbfposadd  28899  dvtan  28902  itg2addnclem  28903  ibladdnclem  28908  itgaddnclem1  28910  iblabsnclem  28915  itggt0cn  28924  ftc1anclem4  28930  ftc1anclem5  28931  ftc1anclem6  28932  ftc1anclem7  28933  ftc1anclem8  28934  dvcncxp1  28937  dvcnsqr  28938  dvasin  28940  dvacos  28941  areacirclem1  28944  arearect  30051  areaquad  30052  lhe4.4ex1a  30063  itgsin0pilem1  30496  wallispilem4  30597  wallispi2  30602  stirlinglem1  30603  stirlinglem3  30605  dirkercncflem2  30633  fourierdlem48  30684  fourierdlem49  30685  fourierdlem56  30692  fourierdlem57  30693  fourierdlem58  30694  fourierdlem60  30696  fourierdlem61  30697  fourierdlem62  30698  fourierdlem107  30743  fouriersw  30761  elfvmptrab  31032

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-10 1777  ax-11 1782  ax-12 1794  ax-13 1955  ax-ext 2432

This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1703  df-clab 2440  df-cleq 2446  df-clel 2449  df-ral 2805  df-opab 4468  df-mpt 4469