Theorem mpteq2ia 4349

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 2422	. . 3
2	1	ax-gen 1586	. 2
3		mpteq2ia.1	. . 3
4	3	rgen 2760	. 2
5		mpteq12f 4343	. 2
6	2, 4, 5	mp2an 657	1

Syntax hints:  ->wi 4  A.wal 1580  =wceq 1687  e.wcel 1749  A.wral 2694  e.cmpt 4325

This theorem is referenced by:  mpteq2i  4350  feqresmpt  5715  fmptap  5870  offres  6541  resixpfo  7260  dfoi  7672  cantnflem1d  7843  cantnflem1  7844  cantnflem1dOLD  7866  cantnflem1OLD  7867  dfceil2  11621  cnrecnv  12595  ackbijnn  13231  harmonic  13261  ege2le3  13315  eirrlem  13426  prmrec  13923  imasdsval2  14394  cayleylem1  15854  pmtrprfval  15930  gsumzsplit  16333  gsumsn  16347  gsum2d  16355  dmdprdsplitlem  16404  coe1sclmul  17499  coe1sclmul2  17501  frlmip  17907  mdetunilem9  18128  leordtvallem1  18518  leordtvallem2  18519  txkgen  18929  cnmpt1st  18945  cnmpt2nd  18946  tmdgsum  19370  tsmssplit  19426  cnfldnm  20058  expcn  20148  pcorev2  20300  pi1xfrcnv  20329  rrxip  20594  mbfi1flim  20901  itg2uba  20921  itg2cnlem1  20939  itg2cnlem2  20940  itgitg2  20984  itgss3  20992  itgless  20994  ibladdlem  20997  itgaddlem1  21000  iblabslem  21005  itggt0  21019  itgcn  21020  limcdif  21051  limcres  21061  cnplimc  21062  dvcobr  21120  dvexp  21127  dveflem  21151  dvef  21152  dvlip  21165  dvlipcn  21166  lhop  21188  tdeglem2  21272  mdegfvalOLD  21274  plyid  21418  coeidp  21471  dgrid  21472  pserdvlem2  21634  abelth  21647  dvrelog  21823  logcn  21833  dvlog  21837  advlog  21840  advlogexp  21841  logtayl  21846  logccv  21849  dvcxp1  21921  dvsqr  21923  resqrcn  21928  loglesqr  21937  dvatan  22071  leibpilem2  22077  leibpi  22078  efrlim  22104  sqrlim  22107  amgmlem  22124  emcllem5  22134  chtublem  22291  logfacrlim2  22306  bposlem6  22369  chto1lb  22468  vmadivsum  22472  dchrvmasumlema  22490  mulogsumlem  22521  logdivsum  22523  logsqvma2  22533  log2sumbnd  22534  selberglem1  22535  selberglem3  22537  selberg  22538  selberg2lem  22540  selberg2  22541  pntrmax  22554  pntrsumo1  22555  selbergr  22558  selbergs  22564  pnt2  22603  pnt  22604  ostth2  22627  ostth  22629  hilnormi  24244  bra0  25033  partfun  25673  gsumsnf  25951  zrhre  26154  qqhre  26155  eulerpartgbij  26458  plymulx  26652  lgamgulmlem2  26719  lgam1  26753  faclim  27254  ptrest  28096  ovoliunnfl  28104  voliunnfl  28106  mbfposadd  28110  dvtan  28113  itg2addnclem  28114  ibladdnclem  28119  itgaddnclem1  28121  iblabsnclem  28126  itggt0cn  28135  ftc1anclem4  28141  ftc1anclem5  28142  ftc1anclem6  28143  ftc1anclem7  28144  ftc1anclem8  28145  dvcncxp1  28148  dvcnsqr  28149  dvasin  28151  dvacos  28152  areacirclem1  28155  arearect  29264  areaquad  29265  lhe4.4ex1a  29276  itgsin0pilem1  29464  wallispilem4  29537  wallispi2  29542  stirlinglem1  29543  stirlinglem3  29545  elfvmptrab  29829  gsumXzsplit  30481  gsumXsn  30495  gsumX2dlem2  30503

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1586  ax-4 1597  ax-5 1661  ax-6 1701  ax-7 1721  ax-10 1768  ax-11 1773  ax-12 1785  ax-13 1934  ax-ext 2403

This theorem depends on definitions:  df-bi 179  df-an 364  df-tru 1355  df-ex 1582  df-nf 1585  df-sb 1694  df-clab 2409  df-cleq 2415  df-clel 2418  df-ral 2699  df-opab 4326  df-mpt 4327