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

Theorem mpteq12 4280
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 1626 . 2  |-  ( A  =  C  ->  A. x  A  =  C )
2 mpteq12f 4277 . 2  |-  ( ( A. x  A  =  C  /\  A. x  e.  A  B  =  D )  ->  (
x  e.  A  |->  B )  =  ( x  e.  C  |->  D ) )
31, 2sylan 458 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 359   A.wal 1549    = wceq 1652   A.wral 2697    e. cmpt 4258
This theorem is referenced by:  mpteq1  4281  mpteqb  5811  fmptcof  5894  mapxpen  7265  sumeq2w  12476  prdsdsval2  13696  prdsdsval3  13697  ablfac2  15637  xkocnv  17836  voliun  19438  itgeq1f  19653  itgeq2  19659  iblcnlem  19670  esumeq2  24423  esumcvg  24466  prodeq2w  25228  bddiblnc  26238
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-6 1744  ax-7 1749  ax-11 1761  ax-12 1950  ax-ext 2416
This theorem depends on definitions:  df-bi 178  df-an 361  df-tru 1328  df-ex 1551  df-nf 1554  df-sb 1659  df-clab 2422  df-cleq 2428  df-clel 2431  df-ral 2702  df-opab 4259  df-mpt 4260
  Copyright terms: Public domain W3C validator