Theorem mpteq12 4531

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

Assertion

Ref	Expression
mpteq12

Distinct variable groups:   ,   ,

Proof of Theorem mpteq12

Step	Hyp	Ref	Expression
1		ax-5 1704	. 2
2		mpteq12f 4528	. 2
3	1, 2	sylan 471	1

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

This theorem is referenced by:  mpteq1  4532  mpteqb  5970  fmptcof  6065  mapxpen  7703  prodeq2w  13719  prdsdsval2  14881  prdsdsval3  14882  ablfac2  17140  mdetunilem9  19122  mdetmul  19125  xkocnv  20315  voliun  21964  itgeq1f  22178  itgeq2  22184  iblcnlem  22195  esumeq2  28049  esumcvg  28092  dvtan  30065  bddiblnc  30085

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