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

Step	Hyp	Ref	Expression
1		mpteq12i.1	. . . 4
2	1	a1i 11	. . 3
3		mpteq12i.2	. . . 4
4	3	a1i 11	. . 3
5	2, 4	mpteq12dv 4530	. 2
6	5	trud 1404	1

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