Theorem mpteq12 4482

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

Assertion

Ref	Expression
mpteq12	|- ( ( A = C /\ A. x e. A B = D ) -> ( x e. A |-> B ) = ( x e. C |-> D ) )

Distinct variable groups:   x, A   x, C

Allowed substitution hints:   B( x)   D( x)

Proof of Theorem mpteq12

Step	Hyp	Ref	Expression
1		ax-5 1671	. 2 |- ( A = C -> A. x A = C )
2		mpteq12f 4479	. 2 |- ( ( A. x A = C /\ A. x e. A B = D ) -> ( x e. A |-> B ) = ( x e. C |-> D ) )
3	1, 2	sylan 471	1 |- ( ( A = C /\ A. x e. A B = D ) -> ( x e. A |-> B ) = ( x e. C |-> D ) )

Syntax hints:   -> wi 4   /\ wa 369   A.wal 1368   = wceq 1370   A.wral 2799   |-> cmpt 4461

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-10 1777  ax-11 1782  ax-12 1794  ax-13 1955  ax-ext 2432

This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1703  df-clab 2440  df-cleq 2446  df-clel 2449  df-ral 2804  df-opab 4462  df-mpt 4463

This theorem is referenced by:  mpteq1  4483  mpteqb  5900  fmptcof  5989  mapxpen  7590  prdsdsval2  14544  prdsdsval3  14545  ablfac2  16715  mdetunilem9  18561  mdetmul  18564  xkocnv  19522  voliun  21171  itgeq1f  21385  itgeq2  21391  iblcnlem  21402  esumeq2  26657  esumcvg  26700  prodeq2w  27589  dvtan  28610  bddiblnc  28630