Theorem reseq1d 6008

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

Syntax hints:   → wi 4   = wceq 1537   ↾ cres 5702

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-rab 3444  df-in 3983  df-res 5712

This theorem is referenced by:  reseq12d  6010  fun2ssres  6623  funcnvres2  6658  fresin  6790  fresaunres2  6793  offres  8024  itunifval  10485  hsmex  10501  gruima  10871  fseq1p1m1  13658  ltweuz  14012  rlimres  15604  lo1res  15605  lo1resb  15610  rlimresb  15611  o1resb  15612  bitsf1ocnv  16490  fsets  17216  setsres  17225  setscom  17227  sscres  17884  resfval2  17957  estrres  18208  symgvalstruct  19438  symgvalstructOLD  19439  gsumzres  19951  gsumzsplit  19969  gsum2dlem2  20013  dpjidcl  20102  pgpfaclem1  20125  funcrngcsetc  20662  funcringcsetc  20696  rhmsubclem1  20707  pwssplit2  21082  pwssplit3  21083  znle2  21595  phssip  21699  mamures  22422  ofco2  22478  mdetunilem9  22647  mdetmul  22650  smadiadetglem1  22698  smadiadetglem2  22699  tmdgsum  24124  tsmsval2  24159  tsmsres  24173  tsmssplit  24181  imasdsf1olem  24404  tmslem  24515  tmslemOLD  24516  sranlm  24726  cmssmscld  25403  srabn  25413  cmscsscms  25426  mbflimsup  25720  dvres  25966  dvres3a  25969  dvmptresicc  25971  dvnres  25987  cpnres  25993  dvcmul  26001  dvcmulf  26002  dvcobr  26003  dvcobrOLD  26004  dvmptres3  26014  dvmptres2  26020  dvcnvlem  26034  dvlip2  26054  ftc2ditglem  26106  itgpowd  26111  aannenlem1  26388  eff1olem  26608  resqrtcn  26810  sqrtcn  26811  rlimcnp2  27027  jensenlem2  27049  ex-res  30473  rabfodom  32533  resf1o  32744  tocycfvres1  33103  tocycfvres2  33104  cycpmconjvlem  33134  cycpmconjslem2  33148  cyc3conja  33150  ply1gsumz  33584  lbsdiflsp0  33639  submatres  33752  zhmnrg  33913  indf1ofs  33990  carsggect  34283  fibp1  34366  actfunsnf1o  34581  cvmliftlem10  35262  cvmlift2lem6  35276  cvmlift2lem12  35282  satf  35321  poimirlem3  37583  ftc1anclem8  37660  ftc2nc  37662  cocnv  37685  cnpwstotbnd  37757  drngoi  37911  aks6d1c6lem2  42128  aks6d1c6lem4  42130  eldioph2  42718  dvsconst  44299  disjf1o  45098  cncfmptss  45508  limsupresuz  45624  liminfresuz  45705  itgsinexplem1  45875  itgcoscmulx  45890  itgiccshift  45901  itgperiod  45902  dirkeritg  46023  dirkercncflem2  46025  dirkercncflem4  46027  fourierdlem16  46044  fourierdlem21  46049  fourierdlem22  46050  fourierdlem28  46056  fourierdlem42  46070  fourierdlem78  46105  fourierdlem81  46108  fourierdlem83  46110  fourierdlem84  46111  fourierdlem90  46117  fourierdlem93  46120  fourierdlem103  46130  fourierdlem104  46131  sge0resrnlem  46324  ismeannd  46388  0ome  46450  hoidmvlelem3  46518  hoidmvlelem4  46519  rhmsubcALTVlem1  48004  aacllem  48895