Theorem mpteq2ia 4325

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 2443	. . 3
2	1	ax-gen 1556	. 2
3		mpteq2ia.1	. . 3
4	3	rgen 2778	. 2
5		mpteq12f 4319	. 2
6	2, 4, 5	mp2an 655	1

Syntax hints:  ->wi 4  A.wal 1550  =wceq 1654  e.wcel 1728  A.wral 2712  e.cmpt 4301

This theorem is referenced by:  mpteq2i  4326  feqresmpt  5828  fmptap  5971  offres  6369  resixpfo  7149  dfoi  7529  cantnflem1d  7693  cantnflem1  7694  cnrecnv  12021  ackbijnn  12658  harmonic  12689  ege2le3  12743  eirrlem  12854  prmrec  13341  imasdsval2  13793  cayleylem1  15161  gsumzsplit  15580  gsumsn  15594  gsum2d  15597  dmdprdsplitlem  15646  coe1sclmul  16725  coe1sclmul2  16727  leordtvallem1  17325  leordtvallem2  17326  txkgen  17735  cnmpt1st  17751  cnmpt2nd  17752  tmdgsum  18176  tsmssplit  18232  cnfldnm  18864  expcn  18953  pcorev2  19104  pi1xfrcnv  19133  mbfi1flim  19664  itg2uba  19684  itg2cnlem1  19702  itg2cnlem2  19703  itgitg2  19747  itgss3  19755  itgless  19757  ibladdlem  19760  itgaddlem1  19763  iblabslem  19768  itggt0  19782  itgcn  19783  limcdif  19814  limcres  19824  cnplimc  19825  dvcobr  19883  dvexp  19890  dveflem  19914  dvef  19915  dvlip  19928  dvlipcn  19929  lhop  19951  tdeglem2  20035  plyid  20179  coeidp  20232  dgrid  20233  pserdvlem2  20395  abelth  20408  dvrelog  20579  logcn  20589  dvlog  20593  advlog  20596  advlogexp  20597  logtayl  20602  logccv  20605  dvcxp1  20677  dvsqr  20679  resqrcn  20684  loglesqr  20693  dvatan  20826  leibpilem2  20832  leibpi  20833  efrlim  20859  sqrlim  20862  amgmlem  20879  emcllem5  20889  chtublem  21046  logfacrlim2  21061  bposlem6  21124  chto1lb  21223  vmadivsum  21227  dchrvmasumlema  21245  mulogsumlem  21276  logdivsum  21278  logsqvma2  21288  log2sumbnd  21289  selberglem1  21290  selberglem3  21292  selberg  21293  selberg2lem  21295  selberg2  21296  pntrmax  21309  pntrsumo1  21310  selbergr  21313  selbergs  21319  pnt2  21358  pnt  21359  ostth2  21382  ostth  21384  hilnormi  22716  bra0  23504  partfun  24135  zrhre  24434  qqhre  24435  eulerpartgbij  24758  lgamgulmlem2  24918  lgam1  24952  faclim  25469  ovoliunnfl  26357  voliunnfl  26359  mbfposadd  26363  dvtan  26366  itg2addnclem  26367  ibladdnclem  26372  itgaddnclem1  26374  iblabsnclem  26379  itggt0cn  26388  ftc1anclem4  26394  ftc1anclem5  26395  ftc1anclem6  26396  ftc1anclem7  26397  ftc1anclem8  26398  dvreasin  26401  dvreacos  26402  areacirclem1  26403  lhe4.4ex1a  27702  itgsin0pilem1  27898  wallispilem4  27971  wallispi2  27976  stirlinglem1  27977  stirlinglem3  27979

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1556  ax-5 1567  ax-17 1628  ax-9 1669  ax-8 1690  ax-6 1747  ax-7 1752  ax-11 1764  ax-12 1954  ax-ext 2424

This theorem depends on definitions:  df-bi 179  df-an 362  df-tru 1329  df-ex 1552  df-nf 1555  df-sb 1661  df-clab 2430  df-cleq 2436  df-clel 2439  df-ral 2717  df-opab 4302  df-mpt 4303