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

Theorem mpteq2i 4774
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 4773 1 (𝑥𝐴𝐵) = (𝑥𝐴𝐶)
Colors of variables: wff setvar class
Syntax hints:   = wceq 1523  wcel 2030  cmpt 4762
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-clab 2638  df-cleq 2644  df-clel 2647  df-ral 2946  df-opab 4746  df-mpt 4763
This theorem is referenced by:  offval22  7298  konigth  9429  ofccat  13754  rlimneg  14421  cbvprod  14689  eirrlem  14976  ndxidOLD  15931  dfpleOLD  16009  lubfval  17025  glbfval  17038  oduglb  17186  odulub  17188  ablfaclem3  18532  mplcoe3  19514  evlsval  19567  gsummoncoe1  19722  znzrh2  19942  matgsum  20291  mat1f1o  20332  scmatscm  20367  mulmarep1gsum1  20427  mdettpos  20465  mp2pm2mplem4  20662  mp2pm2mplem5  20663  mp2pm2mp  20664  cpmidpmat  20726  cnmpt12f  21517  cnmptkc  21530  xkohmeo  21666  qustgpopn  21970  fsumcn  22720  ovolctb  23304  itg2monolem3  23564  dfitg  23581  itg0  23591  iblre  23605  itgreval  23608  iblconst  23629  itgconst  23630  ibladdlem  23631  itgaddlem1  23634  itgfsum  23638  iblabs  23640  itgsplit  23647  dvmptfsum  23783  dvef  23788  dvsincos  23789  dvlipcn  23802  dvfsumge  23830  coemullem  24051  dvtaylp  24169  taylthlem2  24173  pige3  24314  advlogexp  24446  logtayl  24451  loglesqrt  24544  dvatan  24707  basellem2  24853  wlkson  26608  pthsfval  26673  fusgreghash2wsp  27318  rabfmpunirn  29581  eulerpart  30572  trpredlem1  31851  trpred0  31860  neibastop2  32481  ibladdnclem  33596  itgaddnclem1  33598  iblabsnc  33604  iblmulc2nc  33605  ftc1anclem8  33622  dvasin  33626  areacirclem1  33630  lshpkrlem3  34717  lcfrlem39  37187  hdmap1cbv  37409  mzpnegmpt  37624  mzpresrename  37630  areaquad  38119  dfid7  38236  dfrtrcl5  38253  dfrcl4  38285  fsovrfovd  38620  fsovcnvlem  38624  dssmapnvod  38631  lhe4.4ex1a  38845  dvradcnv2  38863  binomcxplemdvbinom  38869  binomcxp  38873  fprodcn  40150  limsup0  40244  dvmptfprod  40478  dvnprodlem2  40480  dvnprodlem3  40481  dvnprod  40482  iblsplit  40500  itgiccshift  40514  itgperiod  40515  stoweidlem17  40552  dirkeritg  40637  dirkercncf  40642  fourierdlem60  40701  fourierdlem61  40702  fourierdlem93  40734  fourierdlem100  40741  fourierdlem109  40750  fourierdlem112  40753  etransclem13  40782  etransclem46  40815  subsaliuncl  40894  sge0xaddlem2  40969  meaiuninc  41016  caratheodorylem1  41061  caratheodory  41063  hoicvrrex  41091  ovnsubadd  41107  sge0hsphoire  41124  hoidmv1le  41129  hoidmvlelem1  41130  hoidmvlelem2  41131  hoidmvlelem3  41132  hoidmvlelem4  41133  hoidmvlelem5  41134  hoidmvle  41135  ovnhoi  41138  hspdifhsp  41151  hspmbllem3  41163  hspmbl  41164  iccvonmbl  41214  vonicc  41220  vonn0ioo  41222  vonn0icc  41223  smfadd  41294  smflimlem4  41303  smflimsuplem1  41347  smflimsup  41355  dflinc2  42524
  Copyright terms: Public domain W3C validator