Theorem mpteq1 4532

Description: An equality theorem for the maps to notation. (Contributed by Mario Carneiro, 16-Dec-2013.)

Assertion

Ref	Expression
mpteq1

Distinct variable groups:   ,   ,

Proof of Theorem mpteq1

Step	Hyp	Ref	Expression
1		eqidd 2458	. . 3
2	1	rgen 2817	. 2
3		mpteq12 4531	. 2
4	2, 3	mpan2 671	1

Syntax hints:  ->wi 4  =wceq 1395  e.wcel 1818  A.wral 2807  e.cmpt 4510

This theorem is referenced by:  mpteq1d  4533  fmptap  6094  mpt2mpt  6394  mpt2mptsx  6863  mpt2mpts  6864  tposf12  6999  oarec  7230  pwfseq  9063  wunex2  9137  wuncval2  9146  wrd2f1tovbij  12898  vrmdfval  16024  pmtrfval  16475  sylow1  16623  sylow2b  16643  sylow3lem5  16651  sylow3  16653  gsumconst  16954  gsum2dlem2  16998  gsum2dOLD  17000  gsumcom2  17003  srgbinomlem4  17194  mvrfval  18076  mplcoe1  18127  mplcoe5  18131  mplcoe2OLD  18133  evlsval  18188  ply1coe  18337  ply1coeOLD  18338  coe1fzgsumd  18344  evls1fval  18356  evl1gsumd  18393  gsumfsum  18484  mavmul0  19054  m2detleiblem3  19131  m2detleiblem4  19132  madugsum  19145  cramer0  19192  pmatcollpw3fi1lem1  19287  restco  19665  cnmpt1t  20166  cnmpt2t  20174  fmval  20444  symgtgp  20600  prdstgpd  20623  dfarea  23290  istrkg2ld  23858  wlknwwlknbij2  24714  wlkiswwlkbij2  24721  wwlkextbij  24733  gsumvsca1  27773  gsumvsca2  27774  indv  28026  gsumesum  28067  esumlub  28068  sitg0  28288  sdclem2  30235  stoweidlem9  31791  usgedgleord  32419  usgedgleordALT  32420

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