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

Theorem mpteq1d 4528
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 4527 . 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 1379    |-> cmpt 4505
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-clab 2453  df-cleq 2459  df-clel 2462  df-ral 2819  df-opab 4506  df-mpt 4507
This theorem is referenced by:  csbmpt2  4782  fmptapd  6085  offval  6531  mpt2sn  6874  mpt2curryd  6998  cantnff  8093  dfac12lem1  8523  ackbij2lem2  8620  swrd00  12608  swrd0val  12611  repswswrd  12719  repswrevw  12721  revco  12763  ccatco  12764  vdwapfval  14348  imasdsval  14770  mrcfval  14863  catidd  14935  curfpropd  15360  pwspjmhm  15818  grpinvfval  15898  psgnfval  16331  psgnfvalfi  16344  odfval  16363  frgpup3lem  16601  gsum2d2  16805  gsumxp  16807  gsumxpOLD  16809  telgsumfzs  16821  dprd2d2  16895  srgbinom  16998  gsummgp0  17057  pwsco1rhm  17187  pwsco2rhm  17188  staffval  17296  asclfval  17782  asclpropd  17794  mpfrcl  17986  evlsval  17987  evls1fval  18155  evls1rhmlem  18157  evl1fval  18163  phlpropd  18485  pjfval  18532  mvmulfval  18839  submafval  18876  mdetfval  18883  nfimdetndef  18886  mdetfval1  18887  mdet0pr  18889  m1detdiag  18894  madufval  18934  minmar1fval  18943  gsummatr01  18956  pmatcollpw3fi1lem2  19083  pmatcollpw3fi1  19084  cpmadugsumlemF  19172  ispnrm  19634  ptval2  19865  ptpjcn  19875  xkoptsub  19918  kqval  19990  pt1hmeo  20070  fmval  20207  tmdgsum  20357  subgtgp  20367  prdstmdd  20385  prdsxmslem2  20795  nmfval  20872  lebnumlem1  21224  limcmpt2  22051  dvcmulf  22111  mdegfval  22223  ulmshft  22547  wwlkextbij  24437  off2  27182  gsummpt2co  27462  esumnul  27727  ofcfval4  27772  measdivcst  27864  omsfval  27933  ofccat  28165  signstfval  28189  signstf0  28193  signstfvn  28194  ftc1anc  29703  tailfval  29821  sdclem2  29866  mzpclval  30289  mzpcompact2  30317  cncfshiftioo  31259  cncfiooicc  31261  dvsinax  31269  iblspltprt  31319  itgspltprt  31325  itgiccshift  31326  dirkercncflem2  31432  fourierdlem90  31525  mgpsumunsn  32047  lmod1zr  32193  erngfset  35613  erngfset-rN  35621  dvhfset  35895  dvhset  35896
  Copyright terms: Public domain W3C validator