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

Theorem mpteq1d 4771
Description: An equality theorem for the maps to notation. (Contributed by Mario Carneiro, 11-Jun-2016.)
Hypothesis
Ref Expression
mpteq1d.1 (𝜑𝐴 = 𝐵)
Assertion
Ref Expression
mpteq1d (𝜑 → (𝑥𝐴𝐶) = (𝑥𝐵𝐶))
Distinct variable groups:   𝑥,𝐴   𝑥,𝐵
Allowed substitution hints:   𝜑(𝑥)   𝐶(𝑥)

Proof of Theorem mpteq1d
StepHypRef Expression
1 mpteq1d.1 . 2 (𝜑𝐴 = 𝐵)
2 mpteq1 4770 . 2 (𝐴 = 𝐵 → (𝑥𝐴𝐶) = (𝑥𝐵𝐶))
31, 2syl 17 1 (𝜑 → (𝑥𝐴𝐶) = (𝑥𝐵𝐶))
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1523  cmpt 4762
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-clab 2638  df-cleq 2644  df-clel 2647  df-ral 2946  df-opab 4746  df-mpt 4763
This theorem is referenced by:  csbmpt2  5040  fmptapd  6478  offval  6946  mpt2sn  7313  mpt2curryd  7440  cantnff  8609  dfac12lem1  9003  ackbij2lem2  9100  swrd00  13463  swrd0val  13466  swrdlend  13477  swrd0  13480  repswswrd  13577  repswrevw  13579  revco  13626  ccatco  13627  ofccat  13754  vdwapfval  15722  imasdsval  16222  mrcfval  16315  catidd  16388  curfpropd  16920  pwspjmhm  17415  grpinvfval  17507  psgnfval  17966  psgnfvalfi  17979  odfval  17998  frgpup3lem  18236  gsum2d2  18419  gsumxp  18421  telgsumfzs  18432  dprd2d2  18489  srgbinom  18591  gsummgp0  18654  pwsco1rhm  18786  pwsco2rhm  18787  staffval  18895  asclfval  19382  asclpropd  19394  mpfrcl  19566  evlsval  19567  evls1rhmlem  19734  evl1fval  19740  phlpropd  20048  pjfval  20098  mvmulfval  20396  submafval  20433  mdetfval  20440  nfimdetndef  20443  mdetfval1  20444  mdet0pr  20446  m1detdiag  20451  madufval  20491  minmar1fval  20500  gsummatr01  20513  pmatcollpw3fi1lem2  20640  pmatcollpw3fi1  20641  cpmadugsumlemF  20729  ispnrm  21191  ptval2  21452  ptpjcn  21462  xkoptsub  21505  kqval  21577  pt1hmeo  21657  fmval  21794  tmdgsum  21946  subgtgp  21956  prdstmdd  21974  prdsxmslem2  22381  nmfval  22440  lebnumlem1  22807  limcmpt2  23693  dvcmulf  23753  mdegfval  23867  ulmshft  24189  wwlksnextbij  26865  off2  29571  gsummpt2co  29908  esumnul  30238  ofcfval4  30295  measdivcst  30416  omsfval  30484  signstfval  30769  signstf0  30773  signstfvn  30774  mrsubffval  31530  mrsubfval  31531  msubfval  31547  elmsubrn  31551  mvhfval  31556  msrfval  31560  fwddifval  32394  tailfval  32492  curf  33517  poimirlem24  33563  ftc1anc  33623  sdclem2  33668  erngfset  36404  erngfset-rN  36412  dvhfset  36686  dvhset  36687  mzpclval  37605  mzpcompact2  37632  fsovrfovd  38620  mptima2  39771  supcnvlimsupmpt  40291  cncfshiftioo  40423  cncfiooicc  40425  dvsinax  40445  iblspltprt  40507  itgspltprt  40513  itgiccshift  40514  dirkercncflem2  40639  fourierdlem90  40731  fourierdlem92  40733  sge0val  40901  sge0prle  40936  sge0ss  40947  sge0iunmptlemfi  40948  sge0p1  40949  sge0iunmptlemre  40950  sge0iunmpt  40953  sge0xp  40964  ismeannd  41002  caratheodorylem1  41061  isomenndlem  41065  hoidmv1lelem2  41127  hoidmvlelem2  41131  hspmbllem2  41162  smflimsuplem1  41347  smflimsuplem4  41350  smflimsuplem7  41353  smflimsup  41355  funcrngcsetc  42323  funcrngcsetcALT  42324  funcringcsetc  42360  mgpsumunsn  42465  lmod1zr  42607
  Copyright terms: Public domain W3C validator