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

Theorem mpteq2da 4287
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 2436 . . 3  |-  A  =  A
21ax-gen 1555 . 2  |-  A. x  A  =  A
3 mpteq2da.1 . . 3  |-  F/ x ph
4 mpteq2da.2 . . . 4  |-  ( (
ph  /\  x  e.  A )  ->  B  =  C )
54ex 424 . . 3  |-  ( ph  ->  ( x  e.  A  ->  B  =  C ) )
63, 5ralrimi 2780 . 2  |-  ( ph  ->  A. x  e.  A  B  =  C )
7 mpteq12f 4278 . 2  |-  ( ( A. x  A  =  A  /\  A. x  e.  A  B  =  C )  ->  (
x  e.  A  |->  B )  =  ( x  e.  A  |->  C ) )
82, 6, 7sylancr 645 1  |-  ( ph  ->  ( x  e.  A  |->  B )  =  ( x  e.  A  |->  C ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 359   A.wal 1549   F/wnf 1553    = wceq 1652    e. wcel 1725   A.wral 2698    e. cmpt 4259
This theorem is referenced by:  mpteq2dva  4288  sumeq1f  12475  sumeq2ii  12480  xkocnv  17839  utopsnneiplem  18270  offval2f  24073  esumf1o  24438  prodeq1f  25227  prodeq2ii  25232  itg2addnclem  26247  ftc1anclem5  26275  mzpsubmpt  26792  mzpexpmpt  26794  refsum2cnlem1  27676  fmuldfeqlem1  27680  stoweidlem2  27719  stoweidlem6  27723  stoweidlem8  27725  stoweidlem17  27734  stoweidlem19  27736  stoweidlem20  27737  stoweidlem21  27738  stoweidlem22  27739  stoweidlem23  27740  stoweidlem32  27749  stoweidlem36  27753  stoweidlem40  27757  stoweidlem41  27758  stoweidlem47  27764  stirlinglem15  27805
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 2417
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 2423  df-cleq 2429  df-clel 2432  df-ral 2703  df-opab 4260  df-mpt 4261
  Copyright terms: Public domain W3C validator