MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  mpteq2i Structured version   Unicode version

Theorem mpteq2i 4372
Description: An equality inference for the maps to notation. (Contributed by Mario Carneiro, 16-Dec-2013.)
Hypothesis
Ref Expression
mpteq2i.1  |-  B  =  C
Assertion
Ref Expression
mpteq2i  |-  ( x  e.  A  |->  B )  =  ( x  e.  A  |->  C )

Proof of Theorem mpteq2i
StepHypRef Expression
1 mpteq2i.1 . . 3  |-  B  =  C
21a1i 11 . 2  |-  ( x  e.  A  ->  B  =  C )
32mpteq2ia 4371 1  |-  ( x  e.  A  |->  B )  =  ( x  e.  A  |->  C )
Colors of variables: wff setvar class
Syntax hints:    = wceq 1364    e. wcel 1761    e. cmpt 4347
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1596  ax-4 1607  ax-5 1675  ax-6 1713  ax-7 1733  ax-10 1780  ax-11 1785  ax-12 1797  ax-13 1948  ax-ext 2422
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1367  df-ex 1592  df-nf 1595  df-sb 1706  df-clab 2428  df-cleq 2434  df-clel 2437  df-ral 2718  df-opab 4348  df-mpt 4349
This theorem is referenced by:  offval22  6651  konigth  8729  rlimneg  13120  eirrlem  13482  ndxid  14191  lubfval  15144  glbfval  15157  oduglb  15305  odulub  15307  ablfaclem3  16578  mplcoe3  17523  mplcoe3OLD  17524  evlsval  17581  znzrh2  17937  mulmarep1gsum1  18343  mdettpos  18376  cnmpt12f  19198  cnmptkc  19211  xkohmeo  19347  divstgpopn  19649  fsumcn  20405  ovolctb  20932  itg2monolem3  21189  dfitg  21206  itg0  21216  iblre  21230  itgreval  21233  iblconst  21254  itgconst  21255  ibladdlem  21256  itgaddlem1  21259  itgfsum  21263  iblabs  21265  itgsplit  21272  dvmptfsum  21406  dvef  21411  dvsincos  21412  dvlipcn  21425  dvfsumge  21453  coemullem  21676  dvtaylp  21794  taylthlem2  21798  pige3  21938  advlogexp  22059  logtayl  22064  loglesqr  22155  dvatan  22289  basellem2  22378  rabfmpunirn  25903  eulerpart  26695  ofccat  26871  cbvprod  27357  trpredlem1  27620  trpred0  27629  ibladdnclem  28373  itgaddnclem1  28375  iblabsnc  28381  iblmulc2nc  28382  ftc1anclem8  28399  dvasin  28405  areacirclem1  28409  neibastop2  28507  mzpnegmpt  29005  mzpresrename  29012  areaquad  29517  lhe4.4ex1a  29528  stoweidlem17  29737  usgreghash2spot  30587  dflinc2  30785  lshpkrlem3  32479  lcfrlem39  34948  hdmap1cbv  35170
  Copyright terms: Public domain W3C validator