Theorem mpteq2da 4537

Description: Slightly more general equality inference for the maps to notation. (Contributed by FL, 14-Sep-2013.) (Revised by Mario Carneiro, 16-Dec-2013.)

Hypotheses

Ref	Expression
mpteq2da.1
mpteq2da.2

Assertion

Ref	Expression
mpteq2da

Proof of Theorem mpteq2da

Step	Hyp	Ref	Expression
1		eqid 2457	. . 3
2	1	ax-gen 1618	. 2
3		mpteq2da.1	. . 3
4		mpteq2da.2	. . . 4
5	4	ex 434	. . 3
6	3, 5	ralrimi 2857	. 2
7		mpteq12f 4528	. 2
8	2, 6, 7	sylancr 663	1

Syntax hints:  ->wi 4  /\wa 369  A.wal 1393  =wceq 1395  F/wnf 1616  e.wcel 1818  A.wral 2807  e.cmpt 4510

This theorem is referenced by:  mpteq2dva  4538  prodeq1f  13715  prodeq2ii  13720  gsumsnfd  16978  gsummoncoe1  18346  cayleyhamilton1  19393  xkocnv  20315  utopsnneiplem  20750  offval2f  27506  fpwrelmap  27556  esumf1o  28061  itg2addnclem  30066  ftc1anclem5  30094  mzpsubmpt  30675  mzpexpmpt  30677  refsum2cnlem1  31412  fmuldfeqlem1  31576  cncfiooicclem1  31696  dvmptfprodlem  31741  stoweidlem2  31784  stoweidlem6  31788  stoweidlem8  31790  stoweidlem17  31799  stoweidlem19  31801  stoweidlem20  31802  stoweidlem21  31803  stoweidlem22  31804  stoweidlem23  31805  stoweidlem32  31814  stoweidlem36  31818  stoweidlem40  31822  stoweidlem41  31823  stoweidlem47  31829  stirlinglem15  31870

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