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

Theorem mpteq12 4099
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-17 1603 . 2  |-  ( A  =  C  ->  A. x  A  =  C )
2 mpteq12f 4096 . 2  |-  ( ( A. x  A  =  C  /\  A. x  e.  A  B  =  D )  ->  (
x  e.  A  |->  B )  =  ( x  e.  C  |->  D ) )
31, 2sylan 457 1  |-  ( ( A  =  C  /\  A. x  e.  A  B  =  D )  ->  (
x  e.  A  |->  B )  =  ( x  e.  C  |->  D ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 358   A.wal 1527    = wceq 1623   A.wral 2543    e. cmpt 4077
This theorem is referenced by:  mpteq1  4100  mpteqb  5614  fmptcof  5692  mapxpen  7027  sumeq2w  12165  prdsdsval2  13383  prdsdsval3  13384  ablfac2  15324  xkocnv  17505  voliun  18911  itgeq1f  19126  itgeq2  19132  iblcnlem  19143  esumeq2  23418  esumcvg  23454  cndprobprob  23641  stoweidlem17  27766
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264
This theorem depends on definitions:  df-bi 177  df-an 360  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-clab 2270  df-cleq 2276  df-clel 2279  df-ral 2548  df-opab 4078  df-mpt 4079
  Copyright terms: Public domain W3C validator