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

Theorem mpteq2i 5211
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 5209 1 (𝑥𝐴𝐵) = (𝑥𝐴𝐶)
Colors of variables: wff setvar class
Syntax hints:   = wceq 1542  wcel 2107  cmpt 5189
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2708
This theorem depends on definitions:  df-bi 206  df-an 398  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2715  df-cleq 2729  df-clel 2815  df-opab 5169  df-mpt 5190
This theorem is referenced by:  offval22  8021  offsplitfpar  8052  konigth  10506  ofccat  14855  rlimneg  15532  cbvprod  15799  eirrlem  16087  lubfval  18240  glbfval  18253  odulub  18297  oduglb  18299  ablfaclem3  19867  znzrh2  20955  mplcoe3  21442  evlsval  21499  gsummoncoe1  21678  matgsum  21789  mat1f1o  21830  scmatscm  21865  mulmarep1gsum1  21925  mdettpos  21963  mp2pm2mplem4  22161  mp2pm2mplem5  22162  mp2pm2mp  22163  cpmidpmat  22225  cnmpt12f  23020  cnmptkc  23033  xkohmeo  23169  qustgpopn  23474  fsumcn  24236  ovolctb  24857  itg2monolem3  25120  dfitg  25137  itg0  25147  iblre  25161  itgreval  25164  iblconst  25185  itgconst  25186  ibladdlem  25187  itgaddlem1  25190  itgfsum  25194  iblabs  25196  itgsplit  25203  dvmptfsum  25342  dvef  25347  dvsincos  25348  dvlipcn  25361  dvfsumge  25389  coemullem  25614  dvtaylp  25732  taylthlem2  25736  pige3ALT  25879  advlogexp  26013  logtayl  26018  loglesqrt  26114  dvatan  26288  basellem2  26434  wlkson  28607  pthsfval  28672  fusgreghash2wsp  29285  rabfmpunirn  31572  zartopn  32459  eulerpart  32985  satf0  33969  neibastop2  34836  ibladdnclem  36137  itgaddnclem1  36139  iblabsnc  36145  iblmulc2nc  36146  ftc1anclem8  36161  dvasin  36165  areacirclem1  36169  lshpkrlem3  37577  lcfrlem39  40047  hdmap1cbv  40268  mzpnegmpt  41070  mzpresrename  41076  areaquad  41553  dfid7  41891  dfrtrcl5  41908  dfrcl4  41955  fsovrfovd  42288  fsovcnvlem  42292  dssmapnvod  42299  lhe4.4ex1a  42616  dvradcnv2  42634  binomcxplemdvbinom  42640  binomcxp  42644  fprodcn  43848  limsup0  43942  dvmptfprod  44193  dvnprodlem2  44195  dvnprodlem3  44196  dvnprod  44197  iblsplit  44214  itgiccshift  44228  itgperiod  44229  stoweidlem17  44265  dirkeritg  44350  dirkercncf  44355  fourierdlem60  44414  fourierdlem61  44415  fourierdlem93  44447  fourierdlem100  44454  fourierdlem109  44463  fourierdlem112  44466  etransclem13  44495  etransclem46  44528  subsaliuncl  44606  sge0xaddlem2  44682  meaiuninc  44729  caratheodorylem1  44774  caratheodory  44776  hoicvrrex  44804  ovnsubadd  44820  sge0hsphoire  44837  hoidmv1le  44842  hoidmvlelem1  44843  hoidmvlelem2  44844  hoidmvlelem3  44845  hoidmvlelem4  44846  hoidmvlelem5  44847  hoidmvle  44848  ovnhoi  44851  hspdifhsp  44864  hspmbllem3  44876  hspmbl  44877  iccvonmbl  44927  vonicc  44933  vonn0ioo  44935  vonn0icc  44936  smfadd  45013  smflimlem4  45022  smflimsuplem1  45068  smflimsup  45076  dflinc2  46498
  Copyright terms: Public domain W3C validator