Theorem mpteq2ia 4400

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 2489	. . 3
2	1	ax-gen 1570	. 2
3		mpteq2ia.1	. . 3
4	3	rgen 2825	. 2
5		mpteq12f 4394	. 2
6	2, 4, 5	mp2an 655	1

Syntax hints:  ->wi 4  A.wal 1564  =wceq 1670  e.wcel 1732  A.wral 2759  e.cmpt 4376

This theorem is referenced by:  mpteq2i  4401  feqresmpt  5761  fmptap  5916  offres  6578  resixpfo  7264  dfoi  7647  cantnflem1d  7811  cantnflem1  7812  dfceil2  11529  cnrecnv  12501  ackbijnn  13138  harmonic  13168  ege2le3  13222  eirrlem  13333  prmrec  13830  imasdsval2  14296  cayleylem1  15693  gsumzsplit  16139  gsumsn  16153  gsum2d  16161  dmdprdsplitlem  16210  coe1sclmul  17299  coe1sclmul2  17301  pmtrprfval  17640  mdetunilem9  17898  leordtvallem1  18288  leordtvallem2  18289  txkgen  18699  cnmpt1st  18715  cnmpt2nd  18716  tmdgsum  19140  tsmssplit  19196  cnfldnm  19828  expcn  19917  pcorev2  20068  pi1xfrcnv  20097  mbfi1flim  20628  itg2uba  20648  itg2cnlem1  20666  itg2cnlem2  20667  itgitg2  20711  itgss3  20719  itgless  20721  ibladdlem  20724  itgaddlem1  20727  iblabslem  20732  itggt0  20746  itgcn  20747  limcdif  20778  limcres  20788  cnplimc  20789  dvcobr  20847  dvexp  20854  dveflem  20878  dvef  20879  dvlip  20892  dvlipcn  20893  lhop  20915  tdeglem2  20999  plyid  21143  coeidp  21196  dgrid  21197  pserdvlem2  21359  abelth  21372  dvrelog  21548  logcn  21558  dvlog  21562  advlog  21565  advlogexp  21566  logtayl  21571  logccv  21574  dvcxp1  21646  dvsqr  21648  resqrcn  21653  loglesqr  21662  dvatan  21796  leibpilem2  21802  leibpi  21803  efrlim  21829  sqrlim  21832  amgmlem  21849  emcllem5  21859  chtublem  22016  logfacrlim2  22031  bposlem6  22094  chto1lb  22193  vmadivsum  22197  dchrvmasumlema  22215  mulogsumlem  22246  logdivsum  22248  logsqvma2  22258  log2sumbnd  22259  selberglem1  22260  selberglem3  22262  selberg  22263  selberg2lem  22265  selberg2  22266  pntrmax  22279  pntrsumo1  22280  selbergr  22283  selbergs  22289  pnt2  22328  pnt  22329  ostth2  22352  ostth  22354  hilnormi  23687  bra0  24476  partfun  25123  gsumsnf  25404  zrhre  25625  qqhre  25626  eulerpartgbij  25929  plymulx  26100  lgamgulmlem2  26162  lgam1  26196  faclim  26704  ovoliunnfl  27613  voliunnfl  27615  mbfposadd  27619  dvtan  27622  itg2addnclem  27623  ibladdnclem  27628  itgaddnclem1  27630  iblabsnclem  27635  itggt0cn  27644  ftc1anclem4  27650  ftc1anclem5  27651  ftc1anclem6  27652  ftc1anclem7  27653  ftc1anclem8  27654  dvcncxp1  27657  dvcnsqr  27658  dvasin  27660  dvacos  27661  areacirclem1  27664  lhe4.4ex1a  28777  itgsin0pilem1  28969  wallispilem4  29042  wallispi2  29047  stirlinglem1  29048  stirlinglem3  29050  elfvmptrab  29336

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1570  ax-4 1581  ax-5 1644  ax-6 1685  ax-7 1705  ax-10 1751  ax-11 1756  ax-12 1768  ax-13 1955  ax-ext 2470

This theorem depends on definitions:  df-bi 179  df-an 362  df-tru 1338  df-ex 1566  df-nf 1569  df-sb 1677  df-clab 2476  df-cleq 2482  df-clel 2485  df-ral 2764  df-opab 4377  df-mpt 4378