Theorem reseq1d 5851

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

Syntax hints:   → wi 4   = wceq 1533   ↾ cres 5556

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1907  ax-6 1966  ax-7 2011  ax-8 2112  ax-9 2120  ax-ext 2793

This theorem depends on definitions:  df-bi 209  df-an 399  df-ex 1777  df-sb 2066  df-clab 2800  df-cleq 2814  df-clel 2893  df-rab 3147  df-in 3942  df-res 5566

This theorem is referenced by:  reseq12d  5853  fun2ssres  6398  funcnvres2  6433  fresin  6546  fresaunres2  6549  offres  7683  itunifval  9837  hsmex  9853  gruima  10223  fseq1p1m1  12980  ltweuz  13328  rlimres  14914  lo1res  14915  lo1resb  14920  rlimresb  14921  o1resb  14922  bitsf1ocnv  15792  fsets  16515  setsres  16524  setscom  16526  sscres  17092  resfval2  17162  estrres  17388  symgvalstruct  18524  gsumzres  19028  gsumzsplit  19046  gsum2dlem2  19090  dpjidcl  19179  pgpfaclem1  19202  pwssplit2  19831  pwssplit3  19832  znle2  20699  phssip  20801  mamures  21000  ofco2  21059  mdetunilem9  21228  mdetmul  21231  smadiadetglem1  21279  smadiadetglem2  21280  tmdgsum  22702  tsmsval2  22737  tsmsres  22751  tsmssplit  22759  imasdsf1olem  22982  tmslem  23091  sranlm  23292  cmssmscld  23952  srabn  23962  cmscsscms  23975  mbflimsup  24266  dvres  24508  dvres3a  24511  dvnres  24527  cpnres  24533  dvcmul  24540  dvcmulf  24541  dvcobr  24542  dvmptres3  24552  dvmptres2  24558  dvcnvlem  24572  dvlip2  24591  ftc2ditglem  24641  aannenlem1  24916  eff1olem  25131  resqrtcn  25329  sqrtcn  25330  rlimcnp2  25543  jensenlem2  25564  ex-res  28219  rabfodom  30265  resf1o  30465  tocycfvres1  30752  tocycfvres2  30753  cycpmconjvlem  30783  cycpmconjslem2  30797  cyc3conja  30799  lbsdiflsp0  31022  submatres  31071  zhmnrg  31208  indf1ofs  31285  carsggect  31576  fibp1  31659  actfunsnf1o  31875  cvmliftlem10  32541  cvmlift2lem6  32555  cvmlift2lem12  32561  satf  32600  trpredeq1  33059  trpredeq2  33060  trpredeq3  33061  poimirlem3  34894  ftc1anclem8  34973  ftc2nc  34975  cocnv  34999  cnpwstotbnd  35074  drngoi  35228  eldioph2  39357  itgpowd  39819  dvsconst  40660  disjf1o  41450  cncfmptss  41866  limsupresuz  41982  liminfresuz  42063  dvmptresicc  42202  itgsinexplem1  42237  itgcoscmulx  42252  itgiccshift  42263  itgperiod  42264  dirkeritg  42386  dirkercncflem2  42388  dirkercncflem4  42390  fourierdlem16  42407  fourierdlem21  42412  fourierdlem22  42413  fourierdlem28  42419  fourierdlem42  42433  fourierdlem78  42468  fourierdlem81  42471  fourierdlem83  42473  fourierdlem84  42474  fourierdlem90  42480  fourierdlem93  42483  fourierdlem103  42493  fourierdlem104  42494  sge0resrnlem  42684  ismeannd  42748  0ome  42810  hoidmvlelem3  42878  hoidmvlelem4  42879  funcrngcsetc  44268  funcringcsetc  44305  rhmsubclem1  44356  rhmsubcALTVlem1  44374  aacllem  44901