Theorem reseq1d 5641

Description: Equality deduction for restrictions. (Contributed by NM, 21-Oct-2014.)

Hypothesis

Ref	Expression
reseqd.1	⊢ (𝜑 → 𝐴 = 𝐵)

Assertion

Ref	Expression
reseq1d	⊢ (𝜑 → (𝐴 ↾ 𝐶) = (𝐵 ↾ 𝐶))

Proof of Theorem reseq1d

Step	Hyp	Ref	Expression
1		reseqd.1	. 2 ⊢ (𝜑 → 𝐴 = 𝐵)
2		reseq1 5636	. 2 ⊢ (𝐴 = 𝐵 → (𝐴 ↾ 𝐶) = (𝐵 ↾ 𝐶))
3	1, 2	syl 17	1 ⊢ (𝜑 → (𝐴 ↾ 𝐶) = (𝐵 ↾ 𝐶))

Syntax hints:   → wi 4   = wceq 1601   ↾ cres 5357

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1839  ax-4 1853  ax-5 1953  ax-6 2021  ax-7 2054  ax-9 2115  ax-10 2134  ax-11 2149  ax-12 2162  ax-ext 2753

This theorem depends on definitions:  df-bi 199  df-an 387  df-or 837  df-tru 1605  df-ex 1824  df-nf 1828  df-sb 2012  df-clab 2763  df-cleq 2769  df-clel 2773  df-nfc 2920  df-v 3399  df-in 3798  df-res 5367

This theorem is referenced by:  reseq12d  5643  fun2ssres  6179  funcnvres2  6214  fresin  6323  fresaunres2  6326  offres  7440  itunifval  9573  hsmex  9589  gruima  9959  fseq1p1m1  12732  ltweuz  13079  rlimres  14697  lo1res  14698  lo1resb  14703  rlimresb  14704  o1resb  14705  bitsf1ocnv  15572  fsets  16288  setsres  16297  setscom  16299  sscres  16868  resfval2  16938  estrresOLD  17164  estrres  17165  psgnunilem5OLD  18298  gsumzres  18696  gsumzsplit  18713  gsum2dlem2  18756  dpjidcl  18844  pgpfaclem1  18867  pwssplit2  19455  pwssplit3  19456  znle2  20297  phssip  20401  mamures  20600  ofco2  20662  mdetunilem9  20831  mdetmul  20834  smadiadetglem1  20883  smadiadetglem2  20884  tmdgsum  22307  tsmsval2  22341  tsmsres  22355  tsmssplit  22363  imasdsf1olem  22586  tmslem  22695  sranlm  22896  cphsscph  23457  cmssmscld  23556  srabn  23566  cmscsscms  23579  mbflimsup  23870  dvres  24112  dvres3a  24115  dvnres  24131  cpnres  24137  dvcmul  24144  dvcmulf  24145  dvcobr  24146  dvmptres3  24156  dvmptres2  24162  dvcnvlem  24176  dvlip2  24195  ftc2ditglem  24245  aannenlem1  24520  eff1olem  24732  resqrtcn  24930  sqrtcn  24931  rlimcnp2  25145  jensenlem2  25166  ex-res  27873  rabfodom  29906  resf1o  30071  lbsdiflsp0  30440  submatres  30470  zhmnrg  30609  indf1ofs  30686  carsggect  30978  fibp1  31062  actfunsnf1o  31284  cvmliftlem10  31875  cvmlift2lem6  31889  cvmlift2lem12  31895  trpredeq1  32308  trpredeq2  32309  trpredeq3  32310  poimirlem3  34022  ftc1anclem8  34101  ftc2nc  34103  cocnv  34129  cnpwstotbnd  34204  drngoi  34358  eldioph2  38267  itgpowd  38740  dvsconst  39467  disjf1o  40283  cncfmptss  40709  limsupresuz  40825  liminfresuz  40906  dvmptresicc  41044  itgsinexplem1  41079  itgcoscmulx  41094  itgiccshift  41105  itgperiod  41106  dirkeritg  41228  dirkercncflem2  41230  dirkercncflem4  41232  fourierdlem16  41249  fourierdlem21  41254  fourierdlem22  41255  fourierdlem28  41261  fourierdlem42  41275  fourierdlem78  41310  fourierdlem81  41313  fourierdlem83  41315  fourierdlem84  41316  fourierdlem90  41322  fourierdlem93  41325  fourierdlem103  41335  fourierdlem104  41336  sge0resrnlem  41526  ismeannd  41590  0ome  41652  hoidmvlelem3  41720  hoidmvlelem4  41721  funcrngcsetc  42995  funcringcsetc  43032  rhmsubclem1  43083  rhmsubcALTVlem1  43101  aacllem  43635