Theorem reseq1d 5817

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

Syntax hints:   → wi 4   = wceq 1538   ↾ cres 5521

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 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-ext 2770

This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-sb 2070  df-clab 2777  df-cleq 2791  df-clel 2870  df-rab 3115  df-in 3888  df-res 5531

This theorem is referenced by:  reseq12d  5819  fun2ssres  6369  funcnvres2  6404  fresin  6521  fresaunres2  6524  offres  7666  itunifval  9827  hsmex  9843  gruima  10213  fseq1p1m1  12976  ltweuz  13324  rlimres  14907  lo1res  14908  lo1resb  14913  rlimresb  14914  o1resb  14915  bitsf1ocnv  15783  fsets  16508  setsres  16517  setscom  16519  sscres  17085  resfval2  17155  estrres  17381  symgvalstruct  18517  gsumzres  19022  gsumzsplit  19040  gsum2dlem2  19084  dpjidcl  19173  pgpfaclem1  19196  pwssplit2  19825  pwssplit3  19826  znle2  20245  phssip  20347  mamures  20997  ofco2  21056  mdetunilem9  21225  mdetmul  21228  smadiadetglem1  21276  smadiadetglem2  21277  tmdgsum  22700  tsmsval2  22735  tsmsres  22749  tsmssplit  22757  imasdsf1olem  22980  tmslem  23089  sranlm  23290  cmssmscld  23954  srabn  23964  cmscsscms  23977  mbflimsup  24270  dvres  24514  dvres3a  24517  dvmptresicc  24519  dvnres  24534  cpnres  24540  dvcmul  24547  dvcmulf  24548  dvcobr  24549  dvmptres3  24559  dvmptres2  24565  dvcnvlem  24579  dvlip2  24598  ftc2ditglem  24648  itgpowd  24653  aannenlem1  24924  eff1olem  25140  resqrtcn  25338  sqrtcn  25339  rlimcnp2  25552  jensenlem2  25573  ex-res  28226  rabfodom  30274  resf1o  30492  tocycfvres1  30802  tocycfvres2  30803  cycpmconjvlem  30833  cycpmconjslem2  30847  cyc3conja  30849  lbsdiflsp0  31110  submatres  31159  zhmnrg  31318  indf1ofs  31395  carsggect  31686  fibp1  31769  actfunsnf1o  31985  cvmliftlem10  32654  cvmlift2lem6  32668  cvmlift2lem12  32674  satf  32713  trpredeq1  33172  trpredeq2  33173  trpredeq3  33174  poimirlem3  35060  ftc1anclem8  35137  ftc2nc  35139  cocnv  35163  cnpwstotbnd  35235  drngoi  35389  eldioph2  39703  dvsconst  41034  disjf1o  41818  cncfmptss  42229  limsupresuz  42345  liminfresuz  42426  itgsinexplem1  42596  itgcoscmulx  42611  itgiccshift  42622  itgperiod  42623  dirkeritg  42744  dirkercncflem2  42746  dirkercncflem4  42748  fourierdlem16  42765  fourierdlem21  42770  fourierdlem22  42771  fourierdlem28  42777  fourierdlem42  42791  fourierdlem78  42826  fourierdlem81  42829  fourierdlem83  42831  fourierdlem84  42832  fourierdlem90  42838  fourierdlem93  42841  fourierdlem103  42851  fourierdlem104  42852  sge0resrnlem  43042  ismeannd  43106  0ome  43168  hoidmvlelem3  43236  hoidmvlelem4  43237  funcrngcsetc  44622  funcringcsetc  44659  rhmsubclem1  44710  rhmsubcALTVlem1  44728  aacllem  45329