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

Theorem mpteq1 4527
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 2468 . . 3  |-  ( x  e.  A  ->  C  =  C )
21rgen 2824 . 2  |-  A. x  e.  A  C  =  C
3 mpteq12 4526 . 2  |-  ( ( A  =  B  /\  A. x  e.  A  C  =  C )  ->  (
x  e.  A  |->  C )  =  ( x  e.  B  |->  C ) )
42, 3mpan2 671 1  |-  ( A  =  B  ->  (
x  e.  A  |->  C )  =  ( x  e.  B  |->  C ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    = wceq 1379    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:  mpteq1d  4528  fmptap  6084  mpt2mpt  6378  mpt2mptsx  6847  mpt2mpts  6848  tposf12  6980  oarec  7211  pwfseq  9042  wunex2  9116  wuncval2  9125  swrdlend  12619  wrd2f1tovbij  12861  vrmdfval  15856  pmtrfval  16281  sylow1  16429  sylow2b  16449  sylow3lem5  16457  sylow3  16459  gsumconst  16757  gsum2dlem2  16801  gsum2dOLD  16803  gsumcom2  16806  srgbinomlem4  16996  mvrfval  17875  mplcoe1  17926  mplcoe5  17930  mplcoe2OLD  17932  evlsval  17987  ply1coe  18136  ply1coeOLD  18137  coe1fzgsumd  18143  evl1gsumd  18192  gsumfsum  18280  mavmul0  18849  m2detleiblem3  18926  m2detleiblem4  18927  madugsum  18940  cramer0  18987  pmatcollpw3fi1lem1  19082  restco  19459  cnmpt1t  19929  cnmpt2t  19937  fmval  20207  symgtgp  20363  prdstgpd  20386  dfarea  23046  istrkg2ld  23614  wlknwwlknbij2  24418  wlkiswwlkbij2  24425  wwlkextbij  24437  gsumvsca1  27464  gsumvsca2  27465  indv  27694  gsumesum  27735  esumlub  27736  sitg0  27956  sdclem2  29866  stoweidlem9  31337  fourierdlem92  31527  usgedgleord  31914  usgedgleordALT  31915
  Copyright terms: Public domain W3C validator