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

Theorem mpteq1d 4480
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 4479 . 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 1370    |-> cmpt 4457
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-10 1777  ax-11 1782  ax-12 1794  ax-13 1955  ax-ext 2432
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1703  df-clab 2440  df-cleq 2446  df-clel 2449  df-ral 2803  df-opab 4458  df-mpt 4459
This theorem is referenced by:  csbmpt2  4730  fmptapd  6010  offval  6436  mpt2curryd  6897  cantnff  7992  dfac12lem1  8422  ackbij2lem2  8519  swrd00  12431  swrd0val  12434  repswswrd  12539  repswrevw  12541  revco  12579  ccatco  12580  vdwapfval  14149  imasdsval  14571  mrcfval  14664  catidd  14736  curfpropd  15161  pwspjmhm  15614  grpinvfval  15694  psgnfval  16124  psgnfvalfi  16137  odfval  16156  frgpup3lem  16394  gsum2d2  16587  gsumxp  16589  gsumxpOLD  16591  dprd2d2  16664  srgbinom  16765  gsummgp0  16821  pwsco1rhm  16948  pwsco2rhm  16949  staffval  17054  asclfval  17527  asclpropd  17538  mpfrcl  17727  evlsval  17728  evls1fval  17878  evls1rhmlem  17880  evl1fval  17886  phlpropd  18208  pjfval  18255  mvmulfval  18479  submafval  18516  mdetfval  18523  nfimdetndef  18526  mdetfval1  18527  mdet0pr  18529  m1detdiag  18534  madufval  18574  minmar1fval  18583  gsummatr01  18596  ispnrm  19074  ptval2  19305  ptpjcn  19315  xkoptsub  19358  kqval  19430  pt1hmeo  19510  fmval  19647  tmdgsum  19797  subgtgp  19807  prdstmdd  19825  prdsxmslem2  20235  nmfval  20312  lebnumlem1  20664  limcmpt2  21491  dvcmulf  21551  mdegfval  21663  ulmshft  21987  off2  26109  gsummpt2co  26393  esumnul  26646  ofcfval4  26691  measdivcst  26783  omsfval  26852  ofccat  27084  signstfval  27108  signstf0  27112  signstfvn  27113  ftc1anc  28622  tailfval  28740  sdclem2  28785  mzpclval  29208  mzpcompact2  29236  wwlkextbij  30512  mpt2sn  30870  mgpsumunsn  30906  telescfzgsum  30961  lmod1zr  31153  pmatcollpw3fi1lem2  31259  pmatcollpw3fi1  31260  cpmadugsumlemF  31347  erngfset  34766  erngfset-rN  34774  dvhfset  35048  dvhset  35049
  Copyright terms: Public domain W3C validator