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

Theorem mpteq2i 4205
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 10 . 2  |-  ( x  e.  A  ->  B  =  C )
32mpteq2ia 4204 1  |-  ( x  e.  A  |->  B )  =  ( x  e.  A  |->  C )
Colors of variables: wff set class
Syntax hints:    = wceq 1647    e. wcel 1715    e. cmpt 4179
This theorem is referenced by:  konigth  8338  rlimneg  12327  eirrlem  12690  ndxid  13377  oduglb  14453  odulub  14455  ablfaclem3  15532  mplcoe3  16420  znzrh2  16716  cnmpt12f  17577  cnmptkc  17590  xkohmeo  17723  divstgpopn  18015  fsumcn  18588  ovolctb  19064  itg2monolem3  19322  dfitg  19339  itg0  19349  iblre  19363  itgreval  19366  iblconst  19387  itgconst  19388  ibladdlem  19389  itgaddlem1  19392  itgfsum  19396  iblabs  19398  itgsplit  19405  dvmptfsum  19537  dvef  19542  dvsincos  19543  dvlipcn  19556  dvfsumge  19584  evlsval  19618  coemullem  19846  dvtaylp  19964  taylthlem2  19968  pige3  20103  advlogexp  20224  logtayl  20229  loglesqr  20320  dvatan  20453  basellem2  20542  rabfmpunirn  23467  cbvprod  24725  trpredlem1  24971  trpred0  24980  itg2addnclem  25675  ibladdnclem  25679  itgaddnclem1  25681  iblabsnc  25687  iblmulc2nc  25688  dvreasin  25698  areacirclem2  25700  neibastop2  25817  mzpnegmpt  26328  mzpresrename  26334  lhe4.4ex1a  27052  stoweidlem17  27272  lshpkrlem3  29373  lcfrlem39  31842  hdmap1cbv  32064
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1551  ax-5 1562  ax-17 1621  ax-9 1659  ax-8 1680  ax-6 1734  ax-7 1739  ax-11 1751  ax-12 1937  ax-ext 2347
This theorem depends on definitions:  df-bi 177  df-an 360  df-tru 1324  df-ex 1547  df-nf 1550  df-sb 1654  df-clab 2353  df-cleq 2359  df-clel 2362  df-ral 2633  df-opab 4180  df-mpt 4181
  Copyright terms: Public domain W3C validator