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

Theorem mpteq2i 4390
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 4389 1  |-  ( x  e.  A  |->  B )  =  ( x  e.  A  |->  C )
Colors of variables: wff setvar class
Syntax hints:    = wceq 1369    e. wcel 1756    e. cmpt 4365
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2423
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-clab 2430  df-cleq 2436  df-clel 2439  df-ral 2735  df-opab 4366  df-mpt 4367
This theorem is referenced by:  offval22  6667  konigth  8748  rlimneg  13139  eirrlem  13501  ndxid  14210  lubfval  15163  glbfval  15176  oduglb  15324  odulub  15326  ablfaclem3  16603  mplcoe3  17560  mplcoe3OLD  17561  evlsval  17620  znzrh2  17993  mulmarep1gsum1  18399  mdettpos  18432  cnmpt12f  19254  cnmptkc  19267  xkohmeo  19403  divstgpopn  19705  fsumcn  20461  ovolctb  20988  itg2monolem3  21245  dfitg  21262  itg0  21272  iblre  21286  itgreval  21289  iblconst  21310  itgconst  21311  ibladdlem  21312  itgaddlem1  21315  itgfsum  21319  iblabs  21321  itgsplit  21328  dvmptfsum  21462  dvef  21467  dvsincos  21468  dvlipcn  21481  dvfsumge  21509  coemullem  21732  dvtaylp  21850  taylthlem2  21854  pige3  21994  advlogexp  22115  logtayl  22120  loglesqr  22211  dvatan  22345  basellem2  22434  rabfmpunirn  25983  eulerpart  26780  ofccat  26956  cbvprod  27443  trpredlem1  27706  trpred0  27715  ibladdnclem  28467  itgaddnclem1  28469  iblabsnc  28475  iblmulc2nc  28476  ftc1anclem8  28493  dvasin  28499  areacirclem1  28503  neibastop2  28601  mzpnegmpt  29099  mzpresrename  29106  areaquad  29611  lhe4.4ex1a  29622  stoweidlem17  29831  usgreghash2spot  30681  gsummoncoe1  30862  matgsum  30881  mp2pm2mplem4  30938  mp2pm2mplem5  30939  mp2pm2mp  30940  pmattomply1fo  30942  pmattomply1mhmlem2  30948  dflinc2  30963  lshpkrlem3  32776  lcfrlem39  35245  hdmap1cbv  35467
  Copyright terms: Public domain W3C validator