Theorem mpteq12 4501

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 1749	. 2 |- ( A = C -> A. x A = C )
2		mpteq12f 4498	. 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 1436   = wceq 1438   A.wral 2776   |-> cmpt 4480

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1666  ax-4 1679  ax-5 1749  ax-6 1795  ax-7 1840  ax-10 1888  ax-11 1893  ax-12 1906  ax-13 2054  ax-ext 2401

This theorem depends on definitions:  df-bi 189  df-an 373  df-tru 1441  df-ex 1661  df-nf 1665  df-sb 1788  df-clab 2409  df-cleq 2415  df-clel 2418  df-ral 2781  df-opab 4481  df-mpt 4482

This theorem is referenced by:  mpteq1  4502  mpteqb  5978  fmptcof  6070  mapxpen  7742  prodeq2w  13959  prdsdsval2  15375  prdsdsval3  15376  ablfac2  17715  mdetunilem9  19637  mdetmul  19640  xkocnv  20821  voliun  22499  itgeq1f  22721  itgeq2  22727  iblcnlem  22738  esumeq2  28859  esumcvg  28909  dvtan  31950  bddiblnc  31970