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

Theorem mpteq1 4249
Description: An equality theorem for the maps to notation. (Contributed by Mario Carneiro, 16-Dec-2013.)
Assertion
Ref Expression
mpteq1  |-  ( A  =  B  ->  (
x  e.  A  |->  C )  =  ( x  e.  B  |->  C ) )
Distinct variable groups:    x, A    x, B
Allowed substitution hint:    C( x)

Proof of Theorem mpteq1
StepHypRef Expression
1 eqidd 2405 . . 3  |-  ( x  e.  A  ->  C  =  C )
21rgen 2731 . 2  |-  A. x  e.  A  C  =  C
3 mpteq12 4248 . 2  |-  ( ( A  =  B  /\  A. x  e.  A  C  =  C )  ->  (
x  e.  A  |->  C )  =  ( x  e.  B  |->  C ) )
42, 3mpan2 653 1  |-  ( A  =  B  ->  (
x  e.  A  |->  C )  =  ( x  e.  B  |->  C ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1649    e. wcel 1721   A.wral 2666    e. cmpt 4226
This theorem is referenced by:  mpteq1d  4250  fmptap  5882  mpt2mpt  6124  mpt2mptsx  6373  mpt2mpts  6374  tposf12  6463  oarec  6764  pwfseq  8495  wunex2  8569  wuncval2  8578  vrmdfval  14756  sylow1  15192  sylow2b  15212  sylow3lem5  15220  sylow3  15222  gsumconst  15487  gsum2d  15501  gsumcom2  15504  mvrfval  16439  mplcoe1  16483  mplcoe2  16485  ply1coe  16639  gsumfsum  16721  restco  17182  cnmpt1t  17650  cnmpt2t  17658  fmval  17928  symgtgp  18084  prdstgpd  18107  evlsval  19893  dfarea  20752  indv  24363  gsumesum  24404  esumlub  24405  sdclem2  26336  pmtrfval  27261  stoweidlem9  27625  swrdltnd  28000
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2385
This theorem depends on definitions:  df-bi 178  df-an 361  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-clab 2391  df-cleq 2397  df-clel 2400  df-ral 2671  df-opab 4227  df-mpt 4228
  Copyright terms: Public domain W3C validator