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

Theorem mpteq2da 4524
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 2454 . . 3  |-  A  =  A
21ax-gen 1623 . 2  |-  A. x  A  =  A
3 mpteq2da.1 . . 3  |-  F/ x ph
4 mpteq2da.2 . . . 4  |-  ( (
ph  /\  x  e.  A )  ->  B  =  C )
54ex 432 . . 3  |-  ( ph  ->  ( x  e.  A  ->  B  =  C ) )
63, 5ralrimi 2854 . 2  |-  ( ph  ->  A. x  e.  A  B  =  C )
7 mpteq12f 4515 . 2  |-  ( ( A. x  A  =  A  /\  A. x  e.  A  B  =  C )  ->  (
x  e.  A  |->  B )  =  ( x  e.  A  |->  C ) )
82, 6, 7sylancr 661 1  |-  ( ph  ->  ( x  e.  A  |->  B )  =  ( x  e.  A  |->  C ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 367   A.wal 1396    = wceq 1398   F/wnf 1621    e. wcel 1823   A.wral 2804    |-> cmpt 4497
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1623  ax-4 1636  ax-5 1709  ax-6 1752  ax-7 1795  ax-10 1842  ax-11 1847  ax-12 1859  ax-13 2004  ax-ext 2432
This theorem depends on definitions:  df-bi 185  df-an 369  df-tru 1401  df-ex 1618  df-nf 1622  df-sb 1745  df-clab 2440  df-cleq 2446  df-clel 2449  df-ral 2809  df-opab 4498  df-mpt 4499
This theorem is referenced by:  mpteq2dva  4525  prodeq1f  13800  prodeq2ii  13805  gsumsnfd  17177  gsummoncoe1  18544  cayleyhamilton1  19563  xkocnv  20484  utopsnneiplem  20919  offval2f  27736  fpwrelmap  27790  gsummpt2d  28009  esumf1o  28282  esum2d  28325  itg2addnclem  30309  ftc1anclem5  30337  mzpsubmpt  30918  mzpexpmpt  30920  refsum2cnlem1  31655  fmuldfeqlem1  31818  cncfiooicclem1  31938  dvmptfprodlem  31983  stoweidlem2  32026  stoweidlem6  32030  stoweidlem8  32032  stoweidlem17  32041  stoweidlem19  32043  stoweidlem20  32044  stoweidlem21  32045  stoweidlem22  32046  stoweidlem23  32047  stoweidlem32  32056  stoweidlem36  32060  stoweidlem40  32064  stoweidlem41  32065  stoweidlem47  32071  stirlinglem15  32112
  Copyright terms: Public domain W3C validator