Theorem reseq1d 5941

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

Syntax hints:   → wi 4   = wceq 1541   ↾ cres 5640

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2702

This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1782  df-sb 2068  df-clab 2709  df-cleq 2723  df-clel 2809  df-rab 3406  df-in 3920  df-res 5650

This theorem is referenced by:  reseq12d  5943  fun2ssres  6551  funcnvres2  6586  fresin  6716  fresaunres2  6719  offres  7921  itunifval  10361  hsmex  10377  gruima  10747  fseq1p1m1  13525  ltweuz  13876  rlimres  15452  lo1res  15453  lo1resb  15458  rlimresb  15459  o1resb  15460  bitsf1ocnv  16335  fsets  17052  setsres  17061  setscom  17063  sscres  17720  resfval2  17793  estrres  18041  symgvalstruct  19192  symgvalstructOLD  19193  gsumzres  19700  gsumzsplit  19718  gsum2dlem2  19762  dpjidcl  19851  pgpfaclem1  19874  pwssplit2  20578  pwssplit3  20579  znle2  20997  phssip  21099  mamures  21776  ofco2  21837  mdetunilem9  22006  mdetmul  22009  smadiadetglem1  22057  smadiadetglem2  22058  tmdgsum  23483  tsmsval2  23518  tsmsres  23532  tsmssplit  23540  imasdsf1olem  23763  tmslem  23874  tmslemOLD  23875  sranlm  24085  cmssmscld  24751  srabn  24761  cmscsscms  24774  mbflimsup  25067  dvres  25312  dvres3a  25315  dvmptresicc  25317  dvnres  25332  cpnres  25338  dvcmul  25345  dvcmulf  25346  dvcobr  25347  dvmptres3  25357  dvmptres2  25363  dvcnvlem  25377  dvlip2  25396  ftc2ditglem  25446  itgpowd  25451  aannenlem1  25725  eff1olem  25941  resqrtcn  26139  sqrtcn  26140  rlimcnp2  26353  jensenlem2  26374  ex-res  29448  rabfodom  31496  resf1o  31715  tocycfvres1  32029  tocycfvres2  32030  cycpmconjvlem  32060  cycpmconjslem2  32074  cyc3conja  32076  ply1gsumz  32368  lbsdiflsp0  32408  submatres  32476  zhmnrg  32637  indf1ofs  32714  carsggect  33007  fibp1  33090  actfunsnf1o  33306  cvmliftlem10  33975  cvmlift2lem6  33989  cvmlift2lem12  33995  satf  34034  poimirlem3  36154  ftc1anclem8  36231  ftc2nc  36233  cocnv  36257  cnpwstotbnd  36329  drngoi  36483  eldioph2  41143  dvsconst  42732  disjf1o  43532  cncfmptss  43948  limsupresuz  44064  liminfresuz  44145  itgsinexplem1  44315  itgcoscmulx  44330  itgiccshift  44341  itgperiod  44342  dirkeritg  44463  dirkercncflem2  44465  dirkercncflem4  44467  fourierdlem16  44484  fourierdlem21  44489  fourierdlem22  44490  fourierdlem28  44496  fourierdlem42  44510  fourierdlem78  44545  fourierdlem81  44548  fourierdlem83  44550  fourierdlem84  44551  fourierdlem90  44557  fourierdlem93  44560  fourierdlem103  44570  fourierdlem104  44571  sge0resrnlem  44764  ismeannd  44828  0ome  44890  hoidmvlelem3  44958  hoidmvlelem4  44959  funcrngcsetc  46416  funcringcsetc  46453  rhmsubclem1  46504  rhmsubcALTVlem1  46522  aacllem  47368