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

Theorem mpteq2i 4669
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 4668 1 (𝑥𝐴𝐵) = (𝑥𝐴𝐶)
Colors of variables: wff setvar class
Syntax hints:   = wceq 1475  wcel 1977  cmpt 4643
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590
This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-ral 2901  df-opab 4644  df-mpt 4645
This theorem is referenced by:  fvmptopab2  6595  offval22  7140  konigth  9270  ofccat  13556  rlimneg  14225  cbvprod  14484  eirrlem  14771  ndxid  15716  dfpleOLD  15789  lubfval  16801  glbfval  16814  oduglb  16962  odulub  16964  ablfaclem3  18309  mplcoe3  19287  evlsval  19340  gsummoncoe1  19495  znzrh2  19713  matgsum  20062  mat1f1o  20103  scmatscm  20138  mulmarep1gsum1  20198  mdettpos  20236  mp2pm2mplem4  20433  mp2pm2mplem5  20434  mp2pm2mp  20435  cpmidpmat  20497  cnmpt12f  21279  cnmptkc  21292  xkohmeo  21428  qustgpopn  21733  fsumcn  22481  ovolctb  23065  itg2monolem3  23325  dfitg  23342  itg0  23352  iblre  23366  itgreval  23369  iblconst  23390  itgconst  23391  ibladdlem  23392  itgaddlem1  23395  itgfsum  23399  iblabs  23401  itgsplit  23408  dvmptfsum  23542  dvef  23547  dvsincos  23548  dvlipcn  23561  dvfsumge  23589  coemullem  23810  dvtaylp  23928  taylthlem2  23932  pige3  24073  advlogexp  24201  logtayl  24206  loglesqrt  24299  dvatan  24462  basellem2  24608  usgreghash2spot  26596  rabfmpunirn  28833  eulerpart  29771  trpredlem1  30971  trpred0  30980  neibastop2  31526  ibladdnclem  32636  itgaddnclem1  32638  iblabsnc  32644  iblmulc2nc  32645  ftc1anclem8  32662  dvasin  32666  areacirclem1  32670  lshpkrlem3  33417  lcfrlem39  35888  hdmap1cbv  36110  mzpnegmpt  36325  mzpresrename  36331  areaquad  36821  dfid7  36938  dfrtrcl5  36955  dfrcl4  36987  fsovrfovd  37323  fsovcnvlem  37327  dssmapnvod  37334  lhe4.4ex1a  37550  dvradcnv2  37568  binomcxplemdvbinom  37574  binomcxp  37578  fprodcn  38667  dvmptfprod  38835  dvnprodlem2  38837  dvnprodlem3  38838  dvnprod  38839  iblsplit  38858  itgiccshift  38872  itgperiod  38873  stoweidlem17  38910  dirkeritg  38995  dirkercncf  39000  fourierdlem60  39059  fourierdlem61  39060  fourierdlem93  39092  fourierdlem100  39099  fourierdlem109  39108  fourierdlem112  39111  etransclem13  39140  etransclem46  39173  subsaliuncl  39252  sge0xaddlem2  39327  meaiuninc  39374  caratheodorylem1  39416  caratheodory  39418  hoicvrrex  39446  ovnsubadd  39462  sge0hsphoire  39479  hoidmv1le  39484  hoidmvlelem1  39485  hoidmvlelem2  39486  hoidmvlelem3  39487  hoidmvlelem4  39488  hoidmvlelem5  39489  hoidmvle  39490  ovnhoi  39493  hspdifhsp  39506  hspmbllem3  39518  hspmbl  39519  iccvonmbl  39570  vonicc  39576  vonn0ioo  39578  vonn0icc  39579  smfadd  39651  smflimlem4  39660  wlkson  40864  fusgreghash2wsp  41502  dflinc2  41993
  Copyright terms: Public domain W3C validator