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

Theorem mpteq2i 4499
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 4498 1  |-  ( x  e.  A  |->  B )  =  ( x  e.  A  |->  C )
Colors of variables: wff setvar class
Syntax hints:    = wceq 1454    e. wcel 1897    |-> cmpt 4474
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1679  ax-4 1692  ax-5 1768  ax-6 1815  ax-7 1861  ax-10 1925  ax-11 1930  ax-12 1943  ax-13 2101  ax-ext 2441
This theorem depends on definitions:  df-bi 190  df-an 377  df-tru 1457  df-ex 1674  df-nf 1678  df-sb 1808  df-clab 2448  df-cleq 2454  df-clel 2457  df-ral 2753  df-opab 4475  df-mpt 4476
This theorem is referenced by:  fvmptopab2  6359  offval22  6898  konigth  9019  rlimneg  13758  cbvprod  14017  eirrlem  14304  ndxid  15190  lubfval  16272  glbfval  16285  oduglb  16433  odulub  16435  ablfaclem3  17768  mplcoe3  18738  evlsval  18790  gsummoncoe1  18946  znzrh2  19164  matgsum  19510  mat1f1o  19551  scmatscm  19586  mulmarep1gsum1  19646  mdettpos  19684  mp2pm2mplem4  19881  mp2pm2mplem5  19882  mp2pm2mp  19883  cpmidpmat  19945  cnmpt12f  20729  cnmptkc  20742  xkohmeo  20878  qustgpopn  21182  fsumcn  21950  ovolctb  22491  itg2monolem3  22758  dfitg  22775  itg0  22785  iblre  22799  itgreval  22802  iblconst  22823  itgconst  22824  ibladdlem  22825  itgaddlem1  22828  itgfsum  22832  iblabs  22834  itgsplit  22841  dvmptfsum  22975  dvef  22980  dvsincos  22981  dvlipcn  22994  dvfsumge  23022  coemullem  23252  dvtaylp  23373  taylthlem2  23377  pige3  23520  advlogexp  23648  logtayl  23653  loglesqrt  23746  dvatan  23909  basellem2  24056  usgreghash2spot  25845  rabfmpunirn  28300  eulerpart  29263  ofccat  29477  trpredlem1  30516  trpred0  30525  neibastop2  31065  ibladdnclem  32042  itgaddnclem1  32044  iblabsnc  32050  iblmulc2nc  32051  ftc1anclem8  32068  dvasin  32072  areacirclem1  32076  lshpkrlem3  32722  lcfrlem39  35193  hdmap1cbv  35415  mzpnegmpt  35630  mzpresrename  35636  areaquad  36145  dfid7  36263  dfrtrcl5  36280  dfrcl4  36312  lhe4.4ex1a  36721  dvradcnv2  36739  binomcxplemdvbinom  36745  binomcxp  36749  dvmptfprod  37857  dvnprodlem2  37859  dvnprodlem3  37860  dvnprod  37861  iblsplit  37880  itgiccshift  37894  itgperiod  37895  stoweidlem17  37914  dirkeritg  38001  dirkercncf  38006  fourierdlem60  38067  fourierdlem61  38068  fourierdlem93  38100  fourierdlem100  38107  fourierdlem109  38116  fourierdlem112  38119  etransclem13  38149  etransclem46  38182  sge0xaddlem2  38313  caratheodorylem1  38384  caratheodory  38386  hoicvrrex  38415  ovnsubadd  38431  sge0hsphoire  38448  hoidmv1le  38453  hoidmvlelem1  38454  hoidmvlelem2  38455  hoidmvlelem3  38456  hoidmvlelem4  38457  hoidmvlelem5  38458  hoidmvle  38459  ovnhoi  38462  hspdifhsp  38475  hspmbllem3  38487  hspmbl  38488  wlkson  39706  dflinc2  40475
  Copyright terms: Public domain W3C validator