MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  mpteq12 Structured version   Unicode version

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
StepHypRef 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 ) )
31, 2sylan 471 1  |-  ( ( A  =  C  /\  A. x  e.  A  B  =  D )  ->  (
x  e.  A  |->  B )  =  ( x  e.  C  |->  D ) )
Colors of variables: wff setvar class
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
  Copyright terms: Public domain W3C validator