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

Theorem mpteq1d 4254
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 4253 . 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 1649    e. cmpt 4230
This theorem is referenced by:  offval  6275  cantnff  7589  dfac12lem1  7983  ackbij2lem2  8080  swrd00  11724  swrd0val  11727  revco  11762  ccatco  11763  vdwapfval  13298  imasdsval  13700  mrcfval  13792  catidd  13864  curfpropd  14289  pwspjmhm  14726  grpinvfval  14802  odfval  15130  frgpup3lem  15368  gsum2d2  15507  gsumxp  15509  dprd2d2  15561  pwsco1rhm  15792  pwsco2rhm  15793  staffval  15894  asclfval  16352  asclpropd  16363  phlpropd  16845  pjfval  16892  ispnrm  17361  ptval2  17590  ptpjcn  17600  xkoptsub  17643  kqval  17715  pt1hmeo  17795  fmval  17932  tmdgsum  18082  subgtgp  18092  prdstmdd  18110  prdsxmslem2  18516  nmfval  18593  lebnumlem1  18943  limcmpt2  19728  dvcmulf  19788  mpfrcl  19896  evlsval  19897  evl1fval  19904  evl1rhm  19906  mdegfval  19942  ulmshft  20263  off2  24011  fmptapd  24018  esumnul  24400  ofcfval4  24445  measdivcst  24536  tailfval  26295  sdclem2  26340  mzpclval  26676  mzpcompact2  26703  psgnfval  27295  mdetfval  27359  erngfset  31285  erngfset-rN  31293  dvhfset  31567  dvhset  31568
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2389
This theorem depends on definitions:  df-bi 178  df-an 361  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-clab 2395  df-cleq 2401  df-clel 2404  df-ral 2675  df-opab 4231  df-mpt 4232
  Copyright terms: Public domain W3C validator