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

Theorem mpteq2i 5144
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 5143 1 (𝑥𝐴𝐵) = (𝑥𝐴𝐶)
Colors of variables: wff setvar class
Syntax hints:   = wceq 1538  wcel 2115  cmpt 5132
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1971  ax-7 2016  ax-8 2117  ax-9 2125  ax-10 2146  ax-12 2179  ax-ext 2796
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2071  df-clab 2803  df-cleq 2817  df-clel 2896  df-ral 3138  df-opab 5115  df-mpt 5133
This theorem is referenced by:  offval22  7779  offsplitfpar  7811  konigth  9989  ofccat  14329  rlimneg  15003  cbvprod  15269  eirrlem  15557  lubfval  17588  glbfval  17601  oduglb  17749  odulub  17751  ablfaclem3  19209  znzrh2  20244  mplcoe3  20713  evlsval  20765  gsummoncoe1  20940  matgsum  21049  mat1f1o  21090  scmatscm  21125  mulmarep1gsum1  21185  mdettpos  21223  mp2pm2mplem4  21420  mp2pm2mplem5  21421  mp2pm2mp  21422  cpmidpmat  21484  cnmpt12f  22277  cnmptkc  22290  xkohmeo  22426  qustgpopn  22731  fsumcn  23481  ovolctb  24100  itg2monolem3  24362  dfitg  24379  itg0  24389  iblre  24403  itgreval  24406  iblconst  24427  itgconst  24428  ibladdlem  24429  itgaddlem1  24432  itgfsum  24436  iblabs  24438  itgsplit  24445  dvmptfsum  24584  dvef  24589  dvsincos  24590  dvlipcn  24603  dvfsumge  24631  coemullem  24853  dvtaylp  24971  taylthlem2  24975  pige3ALT  25118  advlogexp  25252  logtayl  25257  loglesqrt  25353  dvatan  25527  basellem2  25673  wlkson  27452  pthsfval  27516  fusgreghash2wsp  28129  rabfmpunirn  30412  eulerpart  31700  satf0  32679  trpredlem1  33126  trpred0  33135  neibastop2  33769  ibladdnclem  35061  itgaddnclem1  35063  iblabsnc  35069  iblmulc2nc  35070  ftc1anclem8  35085  dvasin  35089  areacirclem1  35093  lshpkrlem3  36356  lcfrlem39  38825  hdmap1cbv  39046  mzpnegmpt  39605  mzpresrename  39611  areaquad  40086  dfid7  40232  dfrtrcl5  40249  dfrcl4  40297  fsovrfovd  40631  fsovcnvlem  40635  dssmapnvod  40642  lhe4.4ex1a  40957  dvradcnv2  40975  binomcxplemdvbinom  40981  binomcxp  40985  fprodcn  42172  limsup0  42266  dvmptfprod  42517  dvnprodlem2  42519  dvnprodlem3  42520  dvnprod  42521  iblsplit  42538  itgiccshift  42552  itgperiod  42553  stoweidlem17  42589  dirkeritg  42674  dirkercncf  42679  fourierdlem60  42738  fourierdlem61  42739  fourierdlem93  42771  fourierdlem100  42778  fourierdlem109  42787  fourierdlem112  42790  etransclem13  42819  etransclem46  42852  subsaliuncl  42928  sge0xaddlem2  43003  meaiuninc  43050  caratheodorylem1  43095  caratheodory  43097  hoicvrrex  43125  ovnsubadd  43141  sge0hsphoire  43158  hoidmv1le  43163  hoidmvlelem1  43164  hoidmvlelem2  43165  hoidmvlelem3  43166  hoidmvlelem4  43167  hoidmvlelem5  43168  hoidmvle  43169  ovnhoi  43172  hspdifhsp  43185  hspmbllem3  43197  hspmbl  43198  iccvonmbl  43248  vonicc  43254  vonn0ioo  43256  vonn0icc  43257  smfadd  43328  smflimlem4  43337  smflimsuplem1  43381  smflimsup  43389  dflinc2  44749
  Copyright terms: Public domain W3C validator