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

Theorem mpteq1d 4361
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 4360 . 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 1362    e. cmpt 4338
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1594  ax-4 1605  ax-5 1669  ax-6 1707  ax-7 1727  ax-10 1774  ax-11 1779  ax-12 1791  ax-13 1942  ax-ext 2414
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1365  df-ex 1590  df-nf 1593  df-sb 1700  df-clab 2420  df-cleq 2426  df-clel 2429  df-ral 2710  df-opab 4339  df-mpt 4340
This theorem is referenced by:  fmptapd  5889  offval  6316  cantnff  7870  dfac12lem1  8300  ackbij2lem2  8397  swrd00  12297  swrd0val  12300  repswswrd  12405  repswrevw  12407  revco  12445  ccatco  12446  vdwapfval  14014  imasdsval  14435  mrcfval  14528  catidd  14600  curfpropd  15025  pwspjmhm  15477  grpinvfval  15555  psgnfval  15985  psgnfvalfi  15998  odfval  16015  frgpup3lem  16253  gsum2d2  16439  gsumxp  16441  gsumxpOLD  16443  dprd2d2  16516  gsummgp0  16633  pwsco1rhm  16753  pwsco2rhm  16754  staffval  16855  asclfval  17326  asclpropd  17337  phlpropd  17925  pjfval  17972  mvmulfval  18194  submafval  18231  mdetfval  18238  nfimdetndef  18241  mdetfval1  18242  mdet0pr  18244  madufval  18284  minmar1fval  18293  gsummatr01  18306  ispnrm  18784  ptval2  19015  ptpjcn  19025  xkoptsub  19068  kqval  19140  pt1hmeo  19220  fmval  19357  tmdgsum  19507  subgtgp  19517  prdstmdd  19535  prdsxmslem2  19945  nmfval  20022  lebnumlem1  20374  limcmpt2  21200  dvcmulf  21260  mpfrcl  21369  evlsval  21370  evl1fval  21377  evl1rhm  21379  mdegfval  21415  ulmshft  21739  off2  25782  gsummpt2co  26100  esumnul  26355  ofcfval4  26400  measdivcst  26492  ofccat  26788  signstfval  26812  signstf0  26816  signstfvn  26817  ftc1anc  28316  tailfval  28434  sdclem2  28479  mzpclval  28903  mzpcompact2  28931  wwlkextbij  30208  mpt2sn  30565  mgpsumunsn  30590  lmod1zr  30741  erngfset  34013  erngfset-rN  34021  dvhfset  34295  dvhset  34296
  Copyright terms: Public domain W3C validator