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

Theorem mpteq2da 4287
 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
StepHypRef Expression
1 eqid 2436 . . 3
21ax-gen 1555 . 2
3 mpteq2da.1 . . 3
4 mpteq2da.2 . . . 4
54ex 424 . . 3
63, 5ralrimi 2780 . 2
7 mpteq12f 4278 . 2
82, 6, 7sylancr 645 1
 Colors of variables: wff set class Syntax hints:   wi 4   wa 359  wal 1549  wnf 1553   wceq 1652   wcel 1725  wral 2698   cmpt 4259 This theorem is referenced by:  mpteq2dva  4288  sumeq1f  12475  sumeq2ii  12480  xkocnv  17839  utopsnneiplem  18270  offval2f  24073  esumf1o  24438  prodeq1f  25227  prodeq2ii  25232  itg2addnclem  26247  ftc1anclem5  26275  mzpsubmpt  26792  mzpexpmpt  26794  refsum2cnlem1  27676  fmuldfeqlem1  27680  stoweidlem2  27719  stoweidlem6  27723  stoweidlem8  27725  stoweidlem17  27734  stoweidlem19  27736  stoweidlem20  27737  stoweidlem21  27738  stoweidlem22  27739  stoweidlem23  27740  stoweidlem32  27749  stoweidlem36  27753  stoweidlem40  27757  stoweidlem41  27758  stoweidlem47  27764  stirlinglem15  27805 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-6 1744  ax-7 1749  ax-11 1761  ax-12 1950  ax-ext 2417 This theorem depends on definitions:  df-bi 178  df-an 361  df-tru 1328  df-ex 1551  df-nf 1554  df-sb 1659  df-clab 2423  df-cleq 2429  df-clel 2432  df-ral 2703  df-opab 4260  df-mpt 4261
 Copyright terms: Public domain W3C validator