Theorem mpteq12 4485

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 1760	. 2 |- ( A = C -> A. x A = C )
2		mpteq12f 4482	. 2 |- ( ( A. x A = C /\ A. x e. A B = D ) -> ( x e. A |-> B ) = ( x e. C |-> D ) )
3	1, 2	sylan 474	1 |- ( ( A = C /\ A. x e. A B = D ) -> ( x e. A |-> B ) = ( x e. C |-> D ) )

Syntax hints:   -> wi 4   /\ wa 371   A.wal 1444   = wceq 1446   A.wral 2739   |-> cmpt 4464

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1671  ax-4 1684  ax-5 1760  ax-6 1807  ax-7 1853  ax-10 1917  ax-11 1922  ax-12 1935  ax-13 2093  ax-ext 2433

This theorem depends on definitions:  df-bi 189  df-an 373  df-tru 1449  df-ex 1666  df-nf 1670  df-sb 1800  df-clab 2440  df-cleq 2446  df-clel 2449  df-ral 2744  df-opab 4465  df-mpt 4466

This theorem is referenced by:  mpteq1  4486  mpteqb  5969  fmptcof  6062  mapxpen  7743  prodeq2w  13978  prdsdsval2  15394  prdsdsval3  15395  ablfac2  17734  mdetunilem9  19657  mdetmul  19660  xkocnv  20841  voliun  22519  itgeq1f  22741  itgeq2  22747  iblcnlem  22758  esumeq2  28869  esumcvg  28919  dvtan  32004  bddiblnc  32024