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

Theorem mpteq1d 4290
Description: An equality theorem for the maps to notation. (Contributed by Mario Carneiro, 11-Jun-2016.)
Hypothesis
Ref Expression
mpteq1d.1  |-  ( ph  ->  A  =  B )
Assertion
Ref Expression
mpteq1d  |-  ( ph  ->  ( x  e.  A  |->  C )  =  ( x  e.  B  |->  C ) )
Distinct variable groups:    x, A    x, B
Allowed substitution hints:    ph( x)    C( x)

Proof of Theorem mpteq1d
StepHypRef Expression
1 mpteq1d.1 . 2  |-  ( ph  ->  A  =  B )
2 mpteq1 4289 . 2  |-  ( A  =  B  ->  (
x  e.  A  |->  C )  =  ( x  e.  B  |->  C ) )
31, 2syl 16 1  |-  ( ph  ->  ( x  e.  A  |->  C )  =  ( x  e.  B  |->  C ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1652    e. cmpt 4266
This theorem is referenced by:  offval  6312  cantnff  7629  dfac12lem1  8023  ackbij2lem2  8120  swrd00  11765  swrd0val  11768  revco  11803  ccatco  11804  vdwapfval  13339  imasdsval  13741  mrcfval  13833  catidd  13905  curfpropd  14330  pwspjmhm  14767  grpinvfval  14843  odfval  15171  frgpup3lem  15409  gsum2d2  15548  gsumxp  15550  dprd2d2  15602  pwsco1rhm  15833  pwsco2rhm  15834  staffval  15935  asclfval  16393  asclpropd  16404  phlpropd  16886  pjfval  16933  ispnrm  17403  ptval2  17633  ptpjcn  17643  xkoptsub  17686  kqval  17758  pt1hmeo  17838  fmval  17975  tmdgsum  18125  subgtgp  18135  prdstmdd  18153  prdsxmslem2  18559  nmfval  18636  lebnumlem1  18986  limcmpt2  19771  dvcmulf  19831  mpfrcl  19939  evlsval  19940  evl1fval  19947  evl1rhm  19949  mdegfval  19985  ulmshft  20306  off2  24054  fmptapd  24061  esumnul  24443  ofcfval4  24488  measdivcst  24579  ftc1anc  26288  tailfval  26401  sdclem2  26446  mzpclval  26782  mzpcompact2  26809  psgnfval  27400  mdetfval  27464  erngfset  31596  erngfset-rN  31604  dvhfset  31878  dvhset  31879
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-6 1744  ax-7 1749  ax-11 1761  ax-12 1950  ax-ext 2417
This theorem depends on definitions:  df-bi 178  df-an 361  df-tru 1328  df-ex 1551  df-nf 1554  df-sb 1659  df-clab 2423  df-cleq 2429  df-clel 2432  df-ral 2710  df-opab 4267  df-mpt 4268
  Copyright terms: Public domain W3C validator