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

Theorem mpteq1 4100
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 2284 . . 3  |-  ( x  e.  A  ->  C  =  C )
21rgen 2608 . 2  |-  A. x  e.  A  C  =  C
3 mpteq12 4099 . 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 1623    e. wcel 1684   A.wral 2543    e. cmpt 4077
This theorem is referenced by:  mpteq1d  4101  fmptap  5710  mpt2mpt  5939  offval  6085  mpt2mptsx  6187  mpt2mpts  6188  tposf12  6259  oarec  6560  cantnff  7375  dfac12lem1  7769  ackbij2lem2  7866  pwfseq  8286  wunex2  8360  wuncval2  8369  swrd00  11451  swrd0val  11454  vdwapfval  13018  imasdsval  13418  pwspjmhm  14444  vrmdfval  14478  grpinvfval  14520  sylow1  14914  sylow2b  14934  sylow3lem5  14942  sylow3  14944  frgpup3lem  15086  gsumconst  15209  gsum2d  15223  gsum2d2  15225  gsumcom2  15226  gsumxp  15227  pwsco1rhm  15510  pwsco2rhm  15511  staffval  15612  asclfval  16074  asclpropd  16085  mvrfval  16165  mplcoe1  16209  mplcoe2  16211  ply1coe  16368  gsumfsum  16439  phlpropd  16559  pjfval  16606  restco  16895  ispnrm  17067  ptval2  17296  ptpjcn  17305  xkoptsub  17348  cnmpt1t  17359  cnmpt2t  17367  kqval  17417  pt1hmeo  17497  fmval  17638  tmdgsum  17778  symgtgp  17784  subgtgp  17788  prdstmdd  17806  prdstgpd  17807  prdsxmslem2  18075  nmfval  18111  lebnumlem1  18459  limcmpt2  19234  dvcmulf  19294  evlsval  19403  evl1fval  19410  evl1rhm  19412  mdegfval  19448  ulmshft  19769  dfarea  20255  fmptapd  23213  indv  23596  ispr1  25156  isprj1  25163  cur1vald  25199  sigadd  25649  fnmulcv  25684  isder  25707  idcatfun  25941  idmor  25946  fnckle  26045  sdclem2  26452  mzpclval  26803  mzpcompact2  26830  pmtrfval  27393  psgnfval  27423  stoweidlem9  27758
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264
This theorem depends on definitions:  df-bi 177  df-an 360  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-clab 2270  df-cleq 2276  df-clel 2279  df-ral 2548  df-opab 4078  df-mpt 4079
  Copyright terms: Public domain W3C validator