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

Theorem mpteq2i 4256
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 4255 1  |-  ( x  e.  A  |->  B )  =  ( x  e.  A  |->  C )
Colors of variables: wff set class
Syntax hints:    = wceq 1649    e. wcel 1721    e. cmpt 4230
This theorem is referenced by:  konigth  8404  rlimneg  12399  eirrlem  12762  ndxid  13449  oduglb  14525  odulub  14527  ablfaclem3  15604  mplcoe3  16488  znzrh2  16785  cnmpt12f  17655  cnmptkc  17668  xkohmeo  17804  divstgpopn  18106  fsumcn  18857  ovolctb  19343  itg2monolem3  19601  dfitg  19618  itg0  19628  iblre  19642  itgreval  19645  iblconst  19666  itgconst  19667  ibladdlem  19668  itgaddlem1  19671  itgfsum  19675  iblabs  19677  itgsplit  19684  dvmptfsum  19816  dvef  19821  dvsincos  19822  dvlipcn  19835  dvfsumge  19863  evlsval  19897  coemullem  20125  dvtaylp  20243  taylthlem2  20247  pige3  20382  advlogexp  20503  logtayl  20508  loglesqr  20599  dvatan  20732  basellem2  20821  rabfmpunirn  24022  cbvprod  25198  trpredlem1  25448  trpred0  25457  ibladdnclem  26164  itgaddnclem1  26166  iblabsnc  26172  iblmulc2nc  26173  dvreasin  26183  areacirclem2  26185  neibastop2  26284  mzpnegmpt  26695  mzpresrename  26701  lhe4.4ex1a  27418  stoweidlem17  27637  usgreghash2spot  28176  lshpkrlem3  29599  lcfrlem39  32068  hdmap1cbv  32290
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2389
This theorem depends on definitions:  df-bi 178  df-an 361  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-clab 2395  df-cleq 2401  df-clel 2404  df-ral 2675  df-opab 4231  df-mpt 4232
  Copyright terms: Public domain W3C validator