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

Theorem mpteq1i 5238
Description: An equality theorem for the maps-to notation. (Contributed by Glauco Siliprandi, 17-Aug-2020.) Remove all disjoint variable conditions. (Revised by SN, 11-Nov-2024.)
Hypothesis
Ref Expression
mpteq1i.1 𝐴 = 𝐵
Assertion
Ref Expression
mpteq1i (𝑥𝐴𝐶) = (𝑥𝐵𝐶)

Proof of Theorem mpteq1i
StepHypRef Expression
1 mpteq1i.1 . . . 4 𝐴 = 𝐵
21a1i 11 . . 3 (⊤ → 𝐴 = 𝐵)
3 eqidd 2738 . . 3 (⊤ → 𝐶 = 𝐶)
42, 3mpteq12dv 5233 . 2 (⊤ → (𝑥𝐴𝐶) = (𝑥𝐵𝐶))
54mptru 1547 1 (𝑥𝐴𝐶) = (𝑥𝐵𝐶)
Colors of variables: wff setvar class
Syntax hints:   = wceq 1540  wtru 1541  cmpt 5225
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2708
This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-opab 5206  df-mpt 5226
This theorem is referenced by:  fmptap  7190  mpompt  7547  offres  8008  mpomptsx  8089  mpompts  8090  pwfseq  10704  wrd2f1tovbij  14999  pmtrprfval  19505  gsum2dlem2  19989  gsumcom2  19993  srgbinomlem4  20226  ply1coe  22302  m2detleiblem3  22635  m2detleiblem4  22636  pmatcollpw3fi1lem1  22792  restco  23172  limcdif  25911  dfarea  27003  nosupcbv  27747  noinfcbv  27762  istrkg2ld  28468  wlknwwlksnbij  29908  wwlksnextbij  29922  clwlknf1oclwwlkn  30103  dfhnorm2  31141  ccatws1f1o  32936  gsumwrd2dccat  33070  algextdeglem4  33761  algextdeglem5  33762  trlset  40163  limsupequzmptlem  45743  sge0iunmptlemfi  46428  sge0iunmpt  46433  hoidmvlelem3  46612  smfmulc1  46811  smflimsuplem2  46836  tposrescnv  48779  swapf1f1o  48981  precoffunc  49066
  Copyright terms: Public domain W3C validator