Theorem mpteq2i 4535

Description: An equality inference for the maps to notation. (Contributed by Mario Carneiro, 16-Dec-2013.)

Hypothesis

Ref	Expression
mpteq2i.1

Assertion

Ref	Expression
mpteq2i

Proof of Theorem mpteq2i

Step	Hyp	Ref	Expression
1		mpteq2i.1	. . 3
2	1	a1i 11	. 2
3	2	mpteq2ia 4534	1

Syntax hints:  =wceq 1395  e.wcel 1818  e.cmpt 4510

This theorem is referenced by:  offval22  6879  konigth  8965  rlimneg  13469  cbvprod  13722  eirrlem  13937  ndxid  14653  lubfval  15608  glbfval  15621  oduglb  15769  odulub  15771  ablfaclem3  17138  mplcoe3  18128  mplcoe3OLD  18129  evlsval  18188  gsummoncoe1  18346  znzrh2  18584  matgsum  18939  mat1f1o  18980  scmatscm  19015  mulmarep1gsum1  19075  mdettpos  19113  mp2pm2mplem4  19310  mp2pm2mplem5  19311  mp2pm2mp  19312  cpmidpmat  19374  cnmpt12f  20167  cnmptkc  20180  xkohmeo  20316  qustgpopn  20618  fsumcn  21374  ovolctb  21901  itg2monolem3  22159  dfitg  22176  itg0  22186  iblre  22200  itgreval  22203  iblconst  22224  itgconst  22225  ibladdlem  22226  itgaddlem1  22229  itgfsum  22233  iblabs  22235  itgsplit  22242  dvmptfsum  22376  dvef  22381  dvsincos  22382  dvlipcn  22395  dvfsumge  22423  coemullem  22647  dvtaylp  22765  taylthlem2  22769  pige3  22910  advlogexp  23036  logtayl  23041  loglesqrt  23132  dvatan  23266  basellem2  23355  usgreghash2spot  25069  rabfmpunirn  27491  eulerpart  28321  ofccat  28497  trpredlem1  29310  trpred0  29319  ibladdnclem  30071  itgaddnclem1  30073  iblabsnc  30079  iblmulc2nc  30080  ftc1anclem8  30097  dvasin  30103  areacirclem1  30107  neibastop2  30179  mzpnegmpt  30676  mzpresrename  30683  areaquad  31184  lhe4.4ex1a  31234  dvradcnv2  31252  binomcxplemdvbinom  31258  binomcxp  31262  dvmptfprod  31742  dvnprodlem2  31744  dvnprodlem3  31745  dvnprod  31746  iblsplit  31765  itgiccshift  31779  itgperiod  31780  stoweidlem17  31799  dirkeritg  31884  dirkercncf  31889  fourierdlem60  31949  fourierdlem61  31950  fourierdlem93  31982  fourierdlem100  31989  fourierdlem109  31998  fourierdlem112  32001  etransclem13  32030  etransclem46  32063  dflinc2  33011  lshpkrlem3  34837  lcfrlem39  37308  hdmap1cbv  37530

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