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

Theorem mpteq2i 4520
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 4519 1  |-  ( x  e.  A  |->  B )  =  ( x  e.  A  |->  C )
Colors of variables: wff setvar class
Syntax hints:    = wceq 1383    e. wcel 1804    |-> cmpt 4495
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1605  ax-4 1618  ax-5 1691  ax-6 1734  ax-7 1776  ax-10 1823  ax-11 1828  ax-12 1840  ax-13 1985  ax-ext 2421
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1386  df-ex 1600  df-nf 1604  df-sb 1727  df-clab 2429  df-cleq 2435  df-clel 2438  df-ral 2798  df-opab 4496  df-mpt 4497
This theorem is referenced by:  offval22  6864  konigth  8947  rlimneg  13451  cbvprod  13704  eirrlem  13919  ndxid  14635  lubfval  15587  glbfval  15600  oduglb  15748  odulub  15750  ablfaclem3  17117  mplcoe3  18107  mplcoe3OLD  18108  evlsval  18167  gsummoncoe1  18325  znzrh2  18562  matgsum  18917  mat1f1o  18958  scmatscm  18993  mulmarep1gsum1  19053  mdettpos  19091  mp2pm2mplem4  19288  mp2pm2mplem5  19289  mp2pm2mp  19290  cpmidpmat  19352  cnmpt12f  20145  cnmptkc  20158  xkohmeo  20294  qustgpopn  20596  fsumcn  21352  ovolctb  21879  itg2monolem3  22137  dfitg  22154  itg0  22164  iblre  22178  itgreval  22181  iblconst  22202  itgconst  22203  ibladdlem  22204  itgaddlem1  22207  itgfsum  22211  iblabs  22213  itgsplit  22220  dvmptfsum  22354  dvef  22359  dvsincos  22360  dvlipcn  22373  dvfsumge  22401  coemullem  22625  dvtaylp  22743  taylthlem2  22747  pige3  22888  advlogexp  23014  logtayl  23019  loglesqrt  23110  dvatan  23244  basellem2  23333  usgreghash2spot  25047  rabfmpunirn  27469  eulerpart  28299  ofccat  28475  trpredlem1  29286  trpred0  29295  ibladdnclem  30047  itgaddnclem1  30049  iblabsnc  30055  iblmulc2nc  30056  ftc1anclem8  30073  dvasin  30079  areacirclem1  30083  neibastop2  30155  mzpnegmpt  30652  mzpresrename  30659  areaquad  31160  lhe4.4ex1a  31210  dvmptfprod  31696  dvnprodlem2  31698  dvnprodlem3  31699  dvnprod  31700  iblsplit  31719  itgiccshift  31733  itgperiod  31734  stoweidlem17  31753  dirkeritg  31838  dirkercncf  31843  fourierdlem60  31903  fourierdlem61  31904  fourierdlem93  31936  fourierdlem100  31943  fourierdlem109  31952  fourierdlem112  31955  etransclem13  31984  etransclem46  32017  dflinc2  32881  lshpkrlem3  34712  lcfrlem39  37183  hdmap1cbv  37405
  Copyright terms: Public domain W3C validator