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

Theorem reseq1d 5303
Description: Equality deduction for restrictions. (Contributed by NM, 21-Oct-2014.)
Hypothesis
Ref Expression
reseqd.1 (𝜑𝐴 = 𝐵)
Assertion
Ref Expression
reseq1d (𝜑 → (𝐴𝐶) = (𝐵𝐶))

Proof of Theorem reseq1d
StepHypRef Expression
1 reseqd.1 . 2 (𝜑𝐴 = 𝐵)
2 reseq1 5298 . 2 (𝐴 = 𝐵 → (𝐴𝐶) = (𝐵𝐶))
31, 2syl 17 1 (𝜑 → (𝐴𝐶) = (𝐵𝐶))
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1474  cres 5030
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-5 1826  ax-6 1874  ax-7 1921  ax-10 2005  ax-11 2020  ax-12 2033  ax-13 2233  ax-ext 2589
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-tru 1477  df-ex 1695  df-nf 1700  df-sb 1867  df-clab 2596  df-cleq 2602  df-clel 2605  df-nfc 2739  df-v 3174  df-in 3546  df-res 5040
This theorem is referenced by:  reseq12d  5305  fun2ssres  5831  funcnvres2  5869  fresin  5971  fresaunres2  5974  offres  7031  itunifval  9098  hsmex  9114  gruima  9480  fseq1p1m1  12238  ltweuz  12577  rlimres  14083  lo1res  14084  lo1resb  14089  rlimresb  14090  o1resb  14091  bitsf1ocnv  14950  fsets  15669  setsres  15675  setscom  15677  sscres  16252  resfval2  16322  estrres  16548  psgnunilem5  17683  gsumzres  18079  gsumzsplit  18096  gsum2dlem2  18139  dpjidcl  18226  pgpfaclem1  18249  pwssplit2  18827  pwssplit3  18828  znle2  19666  mamures  19957  ofco2  20018  mdetunilem9  20187  mdetmul  20190  smadiadetglem1  20238  smadiadetglem2  20239  tmdgsum  21651  tsmsval2  21685  tsmsres  21699  tsmssplit  21707  imasdsf1olem  21929  tmslem  22038  sranlm  22231  srabn  22881  mbflimsup  23156  dvres  23398  dvres3a  23401  dvnres  23417  cpnres  23423  dvcmul  23430  dvcmulf  23431  dvcobr  23432  dvmptres3  23442  dvmptres2  23448  dvcnvlem  23460  dvlip2  23479  ftc2ditglem  23529  aannenlem1  23804  eff1olem  24015  resqrtcn  24207  sqrtcn  24208  rlimcnp2  24410  jensenlem2  24431  ex-res  26456  rabfodom  28534  resf1o  28699  submatres  29006  zhmnrg  29145  indf1ofs  29221  carsggect  29513  fibp1  29596  cvmliftlem10  30336  cvmlift2lem6  30350  cvmlift2lem12  30356  trpredeq1  30770  trpredeq2  30771  trpredeq3  30772  poimirlem3  32378  ftc1anclem8  32458  ftc2nc  32460  cocnv  32486  cnpwstotbnd  32562  drngoi  32716  eldioph2  36139  itgpowd  36615  dvsconst  37347  disjf1o  38169  cncfmptss  38451  dvmptresicc  38606  itgsinexplem1  38642  itgcoscmulx  38658  itgiccshift  38669  itgperiod  38670  dirkeritg  38792  dirkercncflem2  38794  dirkercncflem4  38796  fourierdlem16  38813  fourierdlem21  38818  fourierdlem22  38819  fourierdlem28  38825  fourierdlem42  38839  fourierdlem78  38874  fourierdlem81  38877  fourierdlem83  38879  fourierdlem84  38880  fourierdlem90  38886  fourierdlem93  38889  fourierdlem103  38899  fourierdlem104  38900  sge0resrnlem  39093  ismeannd  39157  0ome  39216  hoidmvlelem3  39284  hoidmvlelem4  39285  funcrngcsetc  41785  funcringcsetc  41822  rhmsubclem1  41873  rhmsubcALTVlem1  41892  aacllem  42312
  Copyright terms: Public domain W3C validator