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

Theorem mpteq2da 4532
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 2467 . . 3  |-  A  =  A
21ax-gen 1601 . 2  |-  A. x  A  =  A
3 mpteq2da.1 . . 3  |-  F/ x ph
4 mpteq2da.2 . . . 4  |-  ( (
ph  /\  x  e.  A )  ->  B  =  C )
54ex 434 . . 3  |-  ( ph  ->  ( x  e.  A  ->  B  =  C ) )
63, 5ralrimi 2864 . 2  |-  ( ph  ->  A. x  e.  A  B  =  C )
7 mpteq12f 4523 . 2  |-  ( ( A. x  A  =  A  /\  A. x  e.  A  B  =  C )  ->  (
x  e.  A  |->  B )  =  ( x  e.  A  |->  C ) )
82, 6, 7sylancr 663 1  |-  ( ph  ->  ( x  e.  A  |->  B )  =  ( x  e.  A  |->  C ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 369   A.wal 1377    = wceq 1379   F/wnf 1599    e. wcel 1767   A.wral 2814    |-> cmpt 4505
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-clab 2453  df-cleq 2459  df-clel 2462  df-ral 2819  df-opab 4506  df-mpt 4507
This theorem is referenced by:  mpteq2dva  4533  gsumsnfd  16769  gsummoncoe1  18117  cayleyhamilton1  19160  xkocnv  20050  utopsnneiplem  20485  offval2f  27178  fpwrelmap  27228  esumf1o  27701  prodeq1f  28617  prodeq2ii  28622  itg2addnclem  29643  ftc1anclem5  29671  mzpsubmpt  30279  mzpexpmpt  30281  refsum2cnlem1  30990  fmuldfeqlem1  31132  cncfiooicclem1  31232  stoweidlem2  31302  stoweidlem6  31306  stoweidlem8  31308  stoweidlem17  31317  stoweidlem19  31319  stoweidlem20  31320  stoweidlem21  31321  stoweidlem22  31322  stoweidlem23  31323  stoweidlem32  31332  stoweidlem36  31336  stoweidlem40  31340  stoweidlem41  31341  stoweidlem47  31347  stirlinglem15  31388  gsumsndf  32018
  Copyright terms: Public domain W3C validator