Theorem reseq1d 5968

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 5963	. 2 ⊢ (𝐴 = 𝐵 → (𝐴 ↾ 𝐶) = (𝐵 ↾ 𝐶))
3	1, 2	syl 18	1 ⊢ (𝜑 → (𝐴 ↾ 𝐶) = (𝐵 ↾ 𝐶))

Syntax hints:   → wi 4   = wceq 1563   ↾ cres 5654

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1818  ax-4 1832  ax-5 1933  ax-6 1990  ax-7 2031  ax-8 2147  ax-9 2155  ax-ext 2737

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1803  df-sb 2094  df-clab 2744  df-cleq 2757  df-clel 2840  df-rab 3418  df-in 3914  df-res 5664

This theorem is referenced by:  reseq12d  5970  fun2ssres  6570  funcnvres2  6605  fresin  6737  fresaunres2  6740  offres  7968  itunifval  10388  hsmex  10404  gruima  10775  fseq1p1m1  13617  ltweuz  13988  rlimres  15599  lo1res  15600  lo1resb  15605  rlimresb  15606  o1resb  15607  bitsf1ocnv  16492  fsets  17219  setsres  17228  setscom  17230  sscres  17870  resfval2  17940  estrres  18185  symgvalstruct  19458  gsumzres  19970  gsumzsplit  19988  gsum2dlem2  20032  dpjidcl  20121  pgpfaclem1  20144  funcrngcsetc  20716  funcringcsetc  20750  rhmsubclem1  20761  pwssplit2  21150  pwssplit3  21151  znle2  21663  phssip  21768  mamures  22515  ofco2  22569  mdetunilem9  22738  mdetmul  22741  smadiadetglem1  22789  smadiadetglem2  22790  tmdgsum  24213  tsmsval2  24248  tsmsres  24262  tsmssplit  24270  imasdsf1olem  24491  tmslem  24600  sranlm  24802  cmssmscld  25470  srabn  25480  cmscsscms  25493  mbflimsup  25786  dvres  26031  dvres3a  26034  dvmptresicc  26036  dvnres  26051  cpnres  26057  dvcmul  26064  dvcmulf  26065  dvcobr  26066  dvmptres3  26076  dvmptres2  26082  dvcnvlem  26096  dvlip2  26115  ftc2ditglem  26165  itgpowd  26170  aannenlem1  26450  eff1olem  26671  resqrtcn  26872  sqrtcn  26873  rlimcnp2  27089  jensenlem2  27110  ex-res  30701  rabfodom  32761  padct  32975  resf1o  32987  indf1ofs  33099  tocycfvres1  33343  tocycfvres2  33344  cycpmconjvlem  33374  cycpmconjslem2  33388  cyc3conja  33390  gsumind  33580  ply1gsumz  33806  evlextv  33849  lbsdiflsp0  33933  submatres  34113  zhmnrg  34272  carsggect  34625  fibp1  34708  actfunsnf1o  34908  cvmliftlem10  35657  cvmlift2lem6  35671  cvmlift2lem12  35677  satf  35716  poimirlem3  38134  ftc1anclem8  38211  ftc2nc  38213  cocnv  38236  cnpwstotbnd  38308  drngoi  38462  aks6d1c6lem2  42800  aks6d1c6lem4  42802  eldioph2  43355  dvsconst  44904  disjf1o  45767  cncfmptss  46161  limsupresuz  46275  liminfresuz  46356  itgsinexplem1  46526  itgcoscmulx  46541  itgiccshift  46552  itgperiod  46553  dirkeritg  46674  dirkercncflem2  46676  dirkercncflem4  46678  fourierdlem16  46695  fourierdlem21  46700  fourierdlem22  46701  fourierdlem28  46707  fourierdlem42  46721  fourierdlem78  46756  fourierdlem81  46759  fourierdlem83  46761  fourierdlem84  46762  fourierdlem90  46768  fourierdlem93  46771  fourierdlem103  46781  fourierdlem104  46782  sge0resrnlem  46975  ismeannd  47039  0ome  47101  hoidmvlelem3  47169  hoidmvlelem4  47170  rhmsubcALTVlem1  48901  aacllem  50430