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

Theorem mpteq2i 4530
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 4529 1  |-  ( x  e.  A  |->  B )  =  ( x  e.  A  |->  C )
Colors of variables: wff setvar class
Syntax hints:    = wceq 1379    e. wcel 1767    |-> cmpt 4505
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-clab 2453  df-cleq 2459  df-clel 2462  df-ral 2819  df-opab 4506  df-mpt 4507
This theorem is referenced by:  offval22  6859  konigth  8940  rlimneg  13428  eirrlem  13794  ndxid  14507  lubfval  15461  glbfval  15474  oduglb  15622  odulub  15624  ablfaclem3  16928  mplcoe3  17899  mplcoe3OLD  17900  evlsval  17959  gsummoncoe1  18117  znzrh2  18351  matgsum  18706  mat1f1o  18747  scmatscm  18782  mulmarep1gsum1  18842  mdettpos  18880  mp2pm2mplem4  19077  mp2pm2mplem5  19078  mp2pm2mp  19079  cpmidpmat  19141  cnmpt12f  19902  cnmptkc  19915  xkohmeo  20051  divstgpopn  20353  fsumcn  21109  ovolctb  21636  itg2monolem3  21894  dfitg  21911  itg0  21921  iblre  21935  itgreval  21938  iblconst  21959  itgconst  21960  ibladdlem  21961  itgaddlem1  21964  itgfsum  21968  iblabs  21970  itgsplit  21977  dvmptfsum  22111  dvef  22116  dvsincos  22117  dvlipcn  22130  dvfsumge  22158  coemullem  22381  dvtaylp  22499  taylthlem2  22503  pige3  22643  advlogexp  22764  logtayl  22769  loglesqrt  22860  dvatan  22994  basellem2  23083  usgreghash2spot  24746  rabfmpunirn  27163  eulerpart  27961  ofccat  28137  cbvprod  28624  trpredlem1  28887  trpred0  28896  ibladdnclem  29648  itgaddnclem1  29650  iblabsnc  29656  iblmulc2nc  29657  ftc1anclem8  29674  dvasin  29680  areacirclem1  29684  neibastop2  29782  mzpnegmpt  30280  mzpresrename  30287  areaquad  30789  lhe4.4ex1a  30834  iblsplit  31284  itgiccshift  31298  itgperiod  31299  stoweidlem17  31317  dirkeritg  31402  dirkercncf  31407  fourierdlem93  31500  fourierdlem100  31507  fourierdlem109  31516  fourierdlem112  31519  dflinc2  32084  lshpkrlem3  33909  lcfrlem39  36378  hdmap1cbv  36600
  Copyright terms: Public domain W3C validator