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

Theorem mpteq2i 4103
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 4102 1  |-  ( x  e.  A  |->  B )  =  ( x  e.  A  |->  C )
Colors of variables: wff set class
Syntax hints:    = wceq 1623    e. wcel 1684    e. cmpt 4077
This theorem is referenced by:  konigth  8191  rlimneg  12120  eirrlem  12482  ndxid  13169  oduglb  14243  odulub  14245  ablfaclem3  15322  mplcoe3  16210  znzrh2  16499  cnmpt12f  17360  cnmptkc  17373  xkohmeo  17506  divstgpopn  17802  fsumcn  18374  ovolctb  18849  itg2monolem3  19107  dfitg  19124  itg0  19134  iblre  19148  itgreval  19151  iblconst  19172  itgconst  19173  ibladdlem  19174  itgaddlem1  19177  itgfsum  19181  iblabs  19183  itgsplit  19190  dvmptfsum  19322  dvef  19327  dvsincos  19328  dvlipcn  19341  dvfsumge  19369  evlsval  19403  coemullem  19631  dvtaylp  19749  taylthlem2  19753  pige3  19885  advlogexp  20002  logtayl  20007  loglesqr  20098  dvatan  20231  basellem2  20319  rabfmpunirn  23217  isibfm  23593  trpredlem1  24230  trpred0  24239  dvreasin  24923  areacirclem2  24925  neibastop2  26310  mzpnegmpt  26822  mzpresrename  26828  lhe4.4ex1a  27546  stoweidlem17  27766  lshpkrlem3  29302  lcfrlem39  31771  hdmap1cbv  31993
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264
This theorem depends on definitions:  df-bi 177  df-an 360  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-clab 2270  df-cleq 2276  df-clel 2279  df-ral 2548  df-opab 4078  df-mpt 4079
  Copyright terms: Public domain W3C validator