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

Theorem mpteq1d 4698
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 4697 . 2 (𝐴 = 𝐵 → (𝑥𝐴𝐶) = (𝑥𝐵𝐶))
31, 2syl 17 1 (𝜑 → (𝑥𝐴𝐶) = (𝑥𝐵𝐶))
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1480  cmpt 4673
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1878  df-clab 2608  df-cleq 2614  df-clel 2617  df-ral 2912  df-opab 4674  df-mpt 4675
This theorem is referenced by:  csbmpt2  4971  fmptapd  6391  offval  6857  mpt2sn  7213  mpt2curryd  7340  cantnff  8515  dfac12lem1  8909  ackbij2lem2  9006  swrd00  13356  swrd0val  13359  swrdlend  13369  swrd0  13372  repswswrd  13468  repswrevw  13470  revco  13517  ccatco  13518  ofccat  13642  vdwapfval  15599  imasdsval  16096  mrcfval  16189  catidd  16262  curfpropd  16794  pwspjmhm  17289  grpinvfval  17381  psgnfval  17841  psgnfvalfi  17854  odfval  17873  frgpup3lem  18111  gsum2d2  18294  gsumxp  18296  telgsumfzs  18307  dprd2d2  18364  srgbinom  18466  gsummgp0  18529  pwsco1rhm  18659  pwsco2rhm  18660  staffval  18768  asclfval  19253  asclpropd  19265  mpfrcl  19437  evlsval  19438  evls1rhmlem  19605  evl1fval  19611  phlpropd  19919  pjfval  19969  mvmulfval  20267  submafval  20304  mdetfval  20311  nfimdetndef  20314  mdetfval1  20315  mdet0pr  20317  m1detdiag  20322  madufval  20362  minmar1fval  20371  gsummatr01  20384  pmatcollpw3fi1lem2  20511  pmatcollpw3fi1  20512  cpmadugsumlemF  20600  ispnrm  21053  ptval2  21314  ptpjcn  21324  xkoptsub  21367  kqval  21439  pt1hmeo  21519  fmval  21657  tmdgsum  21809  subgtgp  21819  prdstmdd  21837  prdsxmslem2  22244  nmfval  22303  lebnumlem1  22668  limcmpt2  23554  dvcmulf  23614  mdegfval  23726  ulmshft  24048  wwlksnextbij  26666  off2  29282  gsummpt2co  29562  esumnul  29888  ofcfval4  29945  measdivcst  30066  omsfval  30134  signstfval  30418  signstf0  30422  signstfvn  30423  mrsubffval  31109  mrsubfval  31110  msubfval  31126  elmsubrn  31130  mvhfval  31135  msrfval  31139  fwddifval  31908  tailfval  32006  curf  33016  poimirlem24  33062  ftc1anc  33122  sdclem2  33167  erngfset  35564  erngfset-rN  35572  dvhfset  35846  dvhset  35847  mzpclval  36765  mzpcompact2  36792  fsovrfovd  37782  mptima2  38929  supcnvlimsupmpt  39374  cncfshiftioo  39406  cncfiooicc  39408  dvsinax  39429  iblspltprt  39493  itgspltprt  39499  itgiccshift  39500  dirkercncflem2  39625  fourierdlem90  39717  fourierdlem92  39719  sge0val  39887  sge0prle  39922  sge0ss  39933  sge0iunmptlemfi  39934  sge0p1  39935  sge0iunmptlemre  39936  sge0iunmpt  39939  sge0xp  39950  ismeannd  39988  caratheodorylem1  40044  isomenndlem  40048  hoidmv1lelem2  40110  hoidmvlelem2  40114  hspmbllem2  40145  smflimsuplem1  40330  smflimsuplem4  40333  smflimsuplem7  40336  smflimsup  40338  funcrngcsetc  41283  funcrngcsetcALT  41284  funcringcsetc  41320  mgpsumunsn  41425  lmod1zr  41567
  Copyright terms: Public domain W3C validator