Theorem mpteq12 4366

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 1670	. 2 |- ( A = C -> A. x A = C )
2		mpteq12f 4363	. 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 1367   = wceq 1369   A.wral 2710   e. cmpt 4345

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2419

This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-clab 2425  df-cleq 2431  df-clel 2434  df-ral 2715  df-opab 4346  df-mpt 4347

This theorem is referenced by:  mpteq1  4367  mpteqb  5783  fmptcof  5872  mapxpen  7469  prdsdsval2  14414  prdsdsval3  14415  ablfac2  16578  mdetunilem9  18401  mdetmul  18404  xkocnv  19362  voliun  21010  itgeq1f  21224  itgeq2  21230  iblcnlem  21241  esumeq2  26444  esumcvg  26487  prodeq2w  27376  dvtan  28395  bddiblnc  28415