Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  mpteq12i Unicode version

Theorem mpteq12i 4536
 Description: An equality inference for the maps to notation. (Contributed by Scott Fenton, 27-Oct-2010.) (Revised by Mario Carneiro, 16-Dec-2013.)
Hypotheses
Ref Expression
mpteq12i.1
mpteq12i.2
Assertion
Ref Expression
mpteq12i

Proof of Theorem mpteq12i
StepHypRef Expression
1 mpteq12i.1 . . . 4
21a1i 11 . . 3
3 mpteq12i.2 . . . 4
43a1i 11 . . 3
52, 4mpteq12dv 4530 . 2
65trud 1404 1
 Colors of variables: wff setvar class Syntax hints:  =wceq 1395   wtru 1396  e.cmpt 4510 This theorem is referenced by:  offres  6795  pmtrprfval  16512  dprdvalOLD  17036  evlsval  18188  madufval  19139  limcdif  22280  dfhnorm2  26039  cdj3lem3  27357  cdj3lem3b  27359  partfun  27516  esumsn  28072  measinb2  28194  eulerpart  28321  fiblem  28337  trlset  35886 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-10 1837  ax-11 1842  ax-12 1854  ax-13 1999  ax-ext 2435 This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1398  df-ex 1613  df-nf 1617  df-sb 1740  df-clab 2443  df-cleq 2449  df-clel 2452  df-ral 2812  df-opab 4511  df-mpt 4512
 Copyright terms: Public domain W3C validator