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

Theorem mpteq2i 4663
Description: An equality inference for the maps to notation. (Contributed by Mario Carneiro, 16-Dec-2013.)
Hypothesis
Ref Expression
mpteq2i.1 𝐵 = 𝐶
Assertion
Ref Expression
mpteq2i (𝑥𝐴𝐵) = (𝑥𝐴𝐶)

Proof of Theorem mpteq2i
StepHypRef Expression
1 mpteq2i.1 . . 3 𝐵 = 𝐶
21a1i 11 . 2 (𝑥𝐴𝐵 = 𝐶)
32mpteq2ia 4662 1 (𝑥𝐴𝐵) = (𝑥𝐴𝐶)
Colors of variables: wff setvar class
Syntax hints:   = wceq 1474  wcel 1976  cmpt 4637
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-5 1826  ax-6 1874  ax-7 1921  ax-10 2005  ax-11 2020  ax-12 2033  ax-13 2233  ax-ext 2589
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-tru 1477  df-ex 1695  df-nf 1700  df-sb 1867  df-clab 2596  df-cleq 2602  df-clel 2605  df-ral 2900  df-opab 4638  df-mpt 4639
This theorem is referenced by:  fvmptopab2  6573  offval22  7117  konigth  9247  ofccat  13502  rlimneg  14171  cbvprod  14430  eirrlem  14717  ndxid  15662  dfpleOLD  15735  lubfval  16747  glbfval  16760  oduglb  16908  odulub  16910  ablfaclem3  18255  mplcoe3  19233  evlsval  19286  gsummoncoe1  19441  znzrh2  19658  matgsum  20004  mat1f1o  20045  scmatscm  20080  mulmarep1gsum1  20140  mdettpos  20178  mp2pm2mplem4  20375  mp2pm2mplem5  20376  mp2pm2mp  20377  cpmidpmat  20439  cnmpt12f  21221  cnmptkc  21234  xkohmeo  21370  qustgpopn  21675  fsumcn  22412  ovolctb  22982  itg2monolem3  23242  dfitg  23259  itg0  23269  iblre  23283  itgreval  23286  iblconst  23307  itgconst  23308  ibladdlem  23309  itgaddlem1  23312  itgfsum  23316  iblabs  23318  itgsplit  23325  dvmptfsum  23459  dvef  23464  dvsincos  23465  dvlipcn  23478  dvfsumge  23506  coemullem  23727  dvtaylp  23845  taylthlem2  23849  pige3  23990  advlogexp  24118  logtayl  24123  loglesqrt  24216  dvatan  24379  basellem2  24525  usgreghash2spot  26362  rabfmpunirn  28639  eulerpart  29577  trpredlem1  30777  trpred0  30786  neibastop2  31332  ibladdnclem  32432  itgaddnclem1  32434  iblabsnc  32440  iblmulc2nc  32441  ftc1anclem8  32458  dvasin  32462  areacirclem1  32466  lshpkrlem3  33213  lcfrlem39  35684  hdmap1cbv  35906  mzpnegmpt  36121  mzpresrename  36127  areaquad  36617  dfid7  36734  dfrtrcl5  36751  dfrcl4  36783  fsovrfovd  37119  fsovcnvlem  37123  dssmapnvod  37130  lhe4.4ex1a  37346  dvradcnv2  37364  binomcxplemdvbinom  37370  binomcxp  37374  fprodcn  38464  dvmptfprod  38632  dvnprodlem2  38634  dvnprodlem3  38635  dvnprod  38636  iblsplit  38655  itgiccshift  38669  itgperiod  38670  stoweidlem17  38707  dirkeritg  38792  dirkercncf  38797  fourierdlem60  38856  fourierdlem61  38857  fourierdlem93  38889  fourierdlem100  38896  fourierdlem109  38905  fourierdlem112  38908  etransclem13  38937  etransclem46  38970  subsaliuncl  39049  sge0xaddlem2  39124  meaiuninc  39171  caratheodorylem1  39213  caratheodory  39215  hoicvrrex  39243  ovnsubadd  39259  sge0hsphoire  39276  hoidmv1le  39281  hoidmvlelem1  39282  hoidmvlelem2  39283  hoidmvlelem3  39284  hoidmvlelem4  39285  hoidmvlelem5  39286  hoidmvle  39287  ovnhoi  39290  hspdifhsp  39303  hspmbllem3  39315  hspmbl  39316  iccvonmbl  39367  vonicc  39373  vonn0ioo  39375  vonn0icc  39376  smfadd  39448  smflimlem4  39457  wlkson  40859  fusgreghash2wsp  41497  dflinc2  41988
  Copyright terms: Public domain W3C validator