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

Theorem mpteq2da 4105
Description: Slightly more general equality inference for the maps to notation. (Contributed by FL, 14-Sep-2013.) (Revised by Mario Carneiro, 16-Dec-2013.)
Hypotheses
Ref Expression
mpteq2da.1  |-  F/ x ph
mpteq2da.2  |-  ( (
ph  /\  x  e.  A )  ->  B  =  C )
Assertion
Ref Expression
mpteq2da  |-  ( ph  ->  ( x  e.  A  |->  B )  =  ( x  e.  A  |->  C ) )

Proof of Theorem mpteq2da
StepHypRef Expression
1 eqid 2283 . . 3  |-  A  =  A
21ax-gen 1533 . 2  |-  A. x  A  =  A
3 mpteq2da.1 . . 3  |-  F/ x ph
4 mpteq2da.2 . . . 4  |-  ( (
ph  /\  x  e.  A )  ->  B  =  C )
54ex 423 . . 3  |-  ( ph  ->  ( x  e.  A  ->  B  =  C ) )
63, 5ralrimi 2624 . 2  |-  ( ph  ->  A. x  e.  A  B  =  C )
7 mpteq12f 4096 . 2  |-  ( ( A. x  A  =  A  /\  A. x  e.  A  B  =  C )  ->  (
x  e.  A  |->  B )  =  ( x  e.  A  |->  C ) )
82, 6, 7sylancr 644 1  |-  ( ph  ->  ( x  e.  A  |->  B )  =  ( x  e.  A  |->  C ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 358   A.wal 1527   F/wnf 1531    = wceq 1623    e. wcel 1684   A.wral 2543    e. cmpt 4077
This theorem is referenced by:  mpteq2dva  4106  sumeq1f  12161  sumeq2ii  12166  xkocnv  17505  offval2f  23233  esumf1o  23429  cnegvex2  25660  rnegvex2  25661  mzpsubmpt  26821  mzpexpmpt  26823  refsum2cnlem1  27708  fmuldfeqlem1  27712  stoweidlem2  27751  stoweidlem4  27753  stoweidlem6  27755  stoweidlem8  27757  stoweidlem17  27766  stoweidlem19  27768  stoweidlem20  27769  stoweidlem21  27770  stoweidlem22  27771  stoweidlem23  27772  stoweidlem32  27781  stoweidlem36  27785  stoweidlem40  27789  stoweidlem41  27790  stoweidlem47  27796  stirlinglem15  27837
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