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

Theorem mpteq1d 4518
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 4517 . 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 1383    |-> cmpt 4495
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1605  ax-4 1618  ax-5 1691  ax-6 1734  ax-7 1776  ax-10 1823  ax-11 1828  ax-12 1840  ax-13 1985  ax-ext 2421
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1386  df-ex 1600  df-nf 1604  df-sb 1727  df-clab 2429  df-cleq 2435  df-clel 2438  df-ral 2798  df-opab 4496  df-mpt 4497
This theorem is referenced by:  csbmpt2  4772  fmptapd  6080  offval  6532  mpt2sn  6876  mpt2curryd  7000  cantnff  8096  dfac12lem1  8526  ackbij2lem2  8623  swrd00  12627  swrd0val  12630  swrdlend  12638  repswswrd  12738  repswrevw  12740  revco  12782  ccatco  12783  vdwapfval  14471  imasdsval  14894  mrcfval  14987  catidd  15059  curfpropd  15481  pwspjmhm  15978  grpinvfval  16067  psgnfval  16504  psgnfvalfi  16517  odfval  16536  frgpup3lem  16774  gsum2d2  16981  gsumxp  16983  gsumxpOLD  16985  telgsumfzs  16997  dprd2d2  17072  srgbinom  17175  gsummgp0  17235  pwsco1rhm  17366  pwsco2rhm  17367  staffval  17475  asclfval  17962  asclpropd  17974  mpfrcl  18166  evlsval  18167  evls1rhmlem  18337  evl1fval  18343  phlpropd  18668  pjfval  18715  mvmulfval  19022  submafval  19059  mdetfval  19066  nfimdetndef  19069  mdetfval1  19070  mdet0pr  19072  m1detdiag  19077  madufval  19117  minmar1fval  19126  gsummatr01  19139  pmatcollpw3fi1lem2  19266  pmatcollpw3fi1  19267  cpmadugsumlemF  19355  ispnrm  19818  ptval2  20080  ptpjcn  20090  xkoptsub  20133  kqval  20205  pt1hmeo  20285  fmval  20422  tmdgsum  20572  subgtgp  20582  prdstmdd  20600  prdsxmslem2  21010  nmfval  21087  lebnumlem1  21439  limcmpt2  22266  dvcmulf  22326  mdegfval  22438  ulmshft  22763  wwlkextbij  24711  off2  27459  gsummpt2co  27749  esumnul  28037  ofcfval4  28082  measdivcst  28174  omsfval  28243  ofccat  28475  signstfval  28499  signstf0  28503  signstfvn  28504  mrsubffval  28845  mrsubfval  28846  msubfval  28862  elmsubrn  28866  mvhfval  28871  msrfval  28875  ftc1anc  30074  tailfval  30166  sdclem2  30211  mzpclval  30633  mzpcompact2  30661  cncfshiftioo  31649  cncfiooicc  31651  dvsinax  31662  iblspltprt  31726  itgspltprt  31732  itgiccshift  31733  dirkercncflem2  31840  fourierdlem90  31933  fourierdlem92  31935  funcrngcsetc  32681  funcrngcsetcALT  32682  funcringcsetc  32715  mgpsumunsn  32819  lmod1zr  32964  erngfset  36400  erngfset-rN  36408  dvhfset  36682  dvhset  36683
  Copyright terms: Public domain W3C validator