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

Theorem mpteq2i 4295
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 4294 1  |-  ( x  e.  A  |->  B )  =  ( x  e.  A  |->  C )
Colors of variables: wff set class
Syntax hints:    = wceq 1653    e. wcel 1726    e. cmpt 4269
This theorem is referenced by:  konigth  8449  rlimneg  12445  eirrlem  12808  ndxid  13495  oduglb  14571  odulub  14573  ablfaclem3  15650  mplcoe3  16534  znzrh2  16831  cnmpt12f  17703  cnmptkc  17716  xkohmeo  17852  divstgpopn  18154  fsumcn  18905  ovolctb  19391  itg2monolem3  19647  dfitg  19664  itg0  19674  iblre  19688  itgreval  19691  iblconst  19712  itgconst  19713  ibladdlem  19714  itgaddlem1  19717  itgfsum  19721  iblabs  19723  itgsplit  19730  dvmptfsum  19864  dvef  19869  dvsincos  19870  dvlipcn  19883  dvfsumge  19911  evlsval  19945  coemullem  20173  dvtaylp  20291  taylthlem2  20295  pige3  20430  advlogexp  20551  logtayl  20556  loglesqr  20647  dvatan  20780  basellem2  20869  rabfmpunirn  24070  cbvprod  25246  trpredlem1  25510  trpred0  25519  ibladdnclem  26275  itgaddnclem1  26277  iblabsnc  26283  iblmulc2nc  26284  ftc1anclem8  26301  dvreasin  26304  areacirclem1  26306  neibastop2  26404  mzpnegmpt  26815  mzpresrename  26821  lhe4.4ex1a  27537  stoweidlem17  27756  usgreghash2spot  28532  lshpkrlem3  29984  lcfrlem39  32453  hdmap1cbv  32675
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1556  ax-5 1567  ax-17 1627  ax-9 1667  ax-8 1688  ax-6 1745  ax-7 1750  ax-11 1762  ax-12 1951  ax-ext 2419
This theorem depends on definitions:  df-bi 179  df-an 362  df-tru 1329  df-ex 1552  df-nf 1555  df-sb 1660  df-clab 2425  df-cleq 2431  df-clel 2434  df-ral 2712  df-opab 4270  df-mpt 4271
  Copyright terms: Public domain W3C validator