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

Theorem mpteq2da 4461
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 2450 . . 3  |-  A  =  A
21ax-gen 1592 . 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 2879 . 2  |-  ( ph  ->  A. x  e.  A  B  =  C )
7 mpteq12f 4452 . 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 1368    = wceq 1370   F/wnf 1590    e. wcel 1757   A.wral 2792    |-> cmpt 4434
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1709  ax-7 1729  ax-10 1776  ax-11 1781  ax-12 1793  ax-13 1944  ax-ext 2429
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1702  df-clab 2436  df-cleq 2442  df-clel 2445  df-ral 2797  df-opab 4435  df-mpt 4436
This theorem is referenced by:  mpteq2dva  4462  xkocnv  19489  utopsnneiplem  19924  offval2f  26103  fpwrelmap  26153  esumf1o  26624  prodeq1f  27541  prodeq2ii  27546  itg2addnclem  28567  ftc1anclem5  28595  mzpsubmpt  29203  mzpexpmpt  29205  refsum2cnlem1  29883  fmuldfeqlem1  29887  stoweidlem2  29921  stoweidlem6  29925  stoweidlem8  29927  stoweidlem17  29936  stoweidlem19  29938  stoweidlem20  29939  stoweidlem21  29940  stoweidlem22  29941  stoweidlem23  29942  stoweidlem32  29951  stoweidlem36  29955  stoweidlem40  29959  stoweidlem41  29960  stoweidlem47  29966  stirlinglem15  30007  gsumsndf  30887  gsummoncoe1  30971  cayleyhamilton1  31333
  Copyright terms: Public domain W3C validator