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

Theorem mpteq1 4202
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 2367 . . 3  |-  ( x  e.  A  ->  C  =  C )
21rgen 2693 . 2  |-  A. x  e.  A  C  =  C
3 mpteq12 4201 . 2  |-  ( ( A  =  B  /\  A. x  e.  A  C  =  C )  ->  (
x  e.  A  |->  C )  =  ( x  e.  B  |->  C ) )
42, 3mpan2 652 1  |-  ( A  =  B  ->  (
x  e.  A  |->  C )  =  ( x  e.  B  |->  C ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1647    e. wcel 1715   A.wral 2628    e. cmpt 4179
This theorem is referenced by:  mpteq1d  4203  fmptap  5823  mpt2mpt  6065  offval  6212  mpt2mptsx  6314  mpt2mpts  6315  tposf12  6401  oarec  6702  cantnff  7522  dfac12lem1  7916  ackbij2lem2  8013  pwfseq  8433  wunex2  8507  wuncval2  8516  swrd00  11652  swrd0val  11655  vdwapfval  13226  imasdsval  13628  pwspjmhm  14654  vrmdfval  14688  grpinvfval  14730  sylow1  15124  sylow2b  15144  sylow3lem5  15152  sylow3  15154  frgpup3lem  15296  gsumconst  15419  gsum2d  15433  gsum2d2  15435  gsumcom2  15436  gsumxp  15437  pwsco1rhm  15720  pwsco2rhm  15721  staffval  15822  asclfval  16284  asclpropd  16295  mvrfval  16375  mplcoe1  16419  mplcoe2  16421  ply1coe  16578  gsumfsum  16656  phlpropd  16776  pjfval  16823  restco  17112  ispnrm  17284  ptval2  17513  ptpjcn  17522  xkoptsub  17565  cnmpt1t  17576  cnmpt2t  17584  kqval  17634  pt1hmeo  17714  fmval  17851  tmdgsum  17991  symgtgp  17997  subgtgp  18001  prdstmdd  18019  prdstgpd  18020  prdsxmslem2  18288  nmfval  18324  lebnumlem1  18674  limcmpt2  19449  dvcmulf  19509  evlsval  19618  evl1fval  19625  evl1rhm  19627  mdegfval  19663  ulmshft  19984  dfarea  20477  fmptapd  23463  indv  23875  gsumesum  23916  esumlub  23917  sdclem2  25959  mzpclval  26309  mzpcompact2  26336  pmtrfval  26899  psgnfval  26929  stoweidlem9  27264
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1551  ax-5 1562  ax-17 1621  ax-9 1659  ax-8 1680  ax-6 1734  ax-7 1739  ax-11 1751  ax-12 1937  ax-ext 2347
This theorem depends on definitions:  df-bi 177  df-an 360  df-tru 1324  df-ex 1547  df-nf 1550  df-sb 1654  df-clab 2353  df-cleq 2359  df-clel 2362  df-ral 2633  df-opab 4180  df-mpt 4181
  Copyright terms: Public domain W3C validator