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

Theorem mpteq1i 5123
Description: An equality theorem for the maps-to notation. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
Hypothesis
Ref Expression
mpteq1i.1 𝐴 = 𝐵
Assertion
Ref Expression
mpteq1i (𝑥𝐴𝐶) = (𝑥𝐵𝐶)
Distinct variable groups:   𝑥,𝐴   𝑥,𝐵
Allowed substitution hint:   𝐶(𝑥)

Proof of Theorem mpteq1i
StepHypRef Expression
1 mpteq1i.1 . 2 𝐴 = 𝐵
2 mpteq1 5121 . 2 (𝐴 = 𝐵 → (𝑥𝐴𝐶) = (𝑥𝐵𝐶))
31, 2ax-mp 5 1 (𝑥𝐴𝐶) = (𝑥𝐵𝐶)
Colors of variables: wff setvar class
Syntax hints:   = wceq 1538  cmpt 5113
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 1911  ax-6 1970  ax-7 2015  ax-8 2114  ax-9 2122  ax-10 2143  ax-12 2176  ax-ext 2773
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 2070  df-clab 2780  df-cleq 2794  df-clel 2873  df-ral 3114  df-opab 5096  df-mpt 5114
This theorem is referenced by:  fmptap  6913  mpompt  7249  offres  7670  mpomptsx  7748  mpompts  7749  pwfseq  10079  wrd2f1tovbij  14319  pmtrprfval  18610  gsum2dlem2  19087  gsumcom2  19091  srgbinomlem4  19289  ply1coe  20928  m2detleiblem3  21237  m2detleiblem4  21238  pmatcollpw3fi1lem1  21394  restco  21772  limcdif  24482  dfarea  25549  istrkg2ld  26257  wlknwwlksnbij  27677  wwlksnextbij  27691  clwlknf1oclwwlkn  27872  dfhnorm2  28908  trlset  37450  limsupequzmptlem  42357  sge0iunmptlemfi  43039  sge0iunmpt  43044  hoidmvlelem3  43223  smfmulc1  43415  smflimsuplem2  43439
  Copyright terms: Public domain W3C validator