Theorem mpteq12 4359

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 1669	. 2 |- ( A = C -> A. x A = C )
2		mpteq12f 4356	. 2 |- ( ( A. x A = C /\ A. x e. A B = D ) -> ( x e. A |-> B ) = ( x e. C |-> D ) )
3	1, 2	sylan 468	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 1360   = wceq 1362   A.wral 2705   e. cmpt 4338

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1594  ax-4 1605  ax-5 1669  ax-6 1707  ax-7 1727  ax-10 1774  ax-11 1779  ax-12 1791  ax-13 1942  ax-ext 2414

This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1365  df-ex 1590  df-nf 1593  df-sb 1700  df-clab 2420  df-cleq 2426  df-clel 2429  df-ral 2710  df-opab 4339  df-mpt 4340

This theorem is referenced by:  mpteq1  4360  mpteqb  5776  fmptcof  5864  mapxpen  7465  prdsdsval2  14404  prdsdsval3  14405  ablfac2  16563  mdetunilem9  18267  mdetmul  18270  xkocnv  19228  voliun  20876  itgeq1f  21090  itgeq2  21096  iblcnlem  21107  esumeq2  26345  esumcvg  26388  prodeq2w  27271  dvtan  28283  bddiblnc  28303