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

Theorem mpteq1d 4368
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 4367 . 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 setvar class
Syntax hints:    -> wi 4    = wceq 1369    e. cmpt 4345
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2419
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-clab 2425  df-cleq 2431  df-clel 2434  df-ral 2715  df-opab 4346  df-mpt 4347
This theorem is referenced by:  csbmpt2  4618  fmptapd  5897  offval  6322  cantnff  7874  dfac12lem1  8304  ackbij2lem2  8401  swrd00  12306  swrd0val  12309  repswswrd  12414  repswrevw  12416  revco  12454  ccatco  12455  vdwapfval  14024  imasdsval  14445  mrcfval  14538  catidd  14610  curfpropd  15035  pwspjmhm  15487  grpinvfval  15567  psgnfval  15997  psgnfvalfi  16010  odfval  16027  frgpup3lem  16265  gsum2d2  16456  gsumxp  16458  gsumxpOLD  16460  dprd2d2  16533  srgbinom  16633  gsummgp0  16689  pwsco1rhm  16810  pwsco2rhm  16811  staffval  16912  asclfval  17385  asclpropd  17396  mpfrcl  17584  evlsval  17585  evls1fval  17734  evls1rhmlem  17736  evl1fval  17742  phlpropd  18064  pjfval  18111  mvmulfval  18333  submafval  18370  mdetfval  18377  nfimdetndef  18380  mdetfval1  18381  mdet0pr  18383  madufval  18423  minmar1fval  18432  gsummatr01  18445  ispnrm  18923  ptval2  19154  ptpjcn  19164  xkoptsub  19207  kqval  19279  pt1hmeo  19359  fmval  19496  tmdgsum  19646  subgtgp  19656  prdstmdd  19674  prdsxmslem2  20084  nmfval  20161  lebnumlem1  20513  limcmpt2  21339  dvcmulf  21399  mdegfval  21511  ulmshft  21835  off2  25927  gsummpt2co  26217  esumnul  26471  ofcfval4  26516  measdivcst  26608  omsfval  26678  ofccat  26910  signstfval  26934  signstf0  26938  signstfvn  26939  ftc1anc  28446  tailfval  28564  sdclem2  28609  mzpclval  29032  mzpcompact2  29060  wwlkextbij  30336  mpt2sn  30693  mgpsumunsn  30728  m1detdiag  30865  lmod1zr  30966  erngfset  34336  erngfset-rN  34344  dvhfset  34618  dvhset  34619
  Copyright terms: Public domain W3C validator