Theorem reseq1d 5845

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

Syntax hints:   → wi 4   = wceq 1531   ↾ cres 5550

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1905  ax-6 1964  ax-7 2009  ax-8 2110  ax-9 2118  ax-ext 2791

This theorem depends on definitions:  df-bi 209  df-an 399  df-ex 1775  df-sb 2064  df-clab 2798  df-cleq 2812  df-clel 2891  df-rab 3145  df-in 3941  df-res 5560

This theorem is referenced by:  reseq12d  5847  fun2ssres  6392  funcnvres2  6427  fresin  6540  fresaunres2  6543  offres  7676  itunifval  9830  hsmex  9846  gruima  10216  fseq1p1m1  12973  ltweuz  13321  rlimres  14907  lo1res  14908  lo1resb  14913  rlimresb  14914  o1resb  14915  bitsf1ocnv  15785  fsets  16508  setsres  16517  setscom  16519  sscres  17085  resfval2  17155  estrres  17381  symgvalstruct  18517  gsumzres  19021  gsumzsplit  19039  gsum2dlem2  19083  dpjidcl  19172  pgpfaclem1  19195  pwssplit2  19824  pwssplit3  19825  znle2  20692  phssip  20794  mamures  20993  ofco2  21052  mdetunilem9  21221  mdetmul  21224  smadiadetglem1  21272  smadiadetglem2  21273  tmdgsum  22695  tsmsval2  22730  tsmsres  22744  tsmssplit  22752  imasdsf1olem  22975  tmslem  23084  sranlm  23285  cmssmscld  23945  srabn  23955  cmscsscms  23968  mbflimsup  24259  dvres  24501  dvres3a  24504  dvnres  24520  cpnres  24526  dvcmul  24533  dvcmulf  24534  dvcobr  24535  dvmptres3  24545  dvmptres2  24551  dvcnvlem  24565  dvlip2  24584  ftc2ditglem  24634  aannenlem1  24909  eff1olem  25124  resqrtcn  25322  sqrtcn  25323  rlimcnp2  25536  jensenlem2  25557  ex-res  28212  rabfodom  30258  resf1o  30458  tocycfvres1  30745  tocycfvres2  30746  cycpmconjvlem  30776  cycpmconjslem2  30790  cyc3conja  30792  lbsdiflsp0  31015  submatres  31064  zhmnrg  31201  indf1ofs  31278  carsggect  31569  fibp1  31652  actfunsnf1o  31868  cvmliftlem10  32534  cvmlift2lem6  32548  cvmlift2lem12  32554  satf  32593  trpredeq1  33052  trpredeq2  33053  trpredeq3  33054  poimirlem3  34887  ftc1anclem8  34966  ftc2nc  34968  cocnv  34992  cnpwstotbnd  35067  drngoi  35221  eldioph2  39349  itgpowd  39811  dvsconst  40652  disjf1o  41441  cncfmptss  41857  limsupresuz  41973  liminfresuz  42054  dvmptresicc  42193  itgsinexplem1  42228  itgcoscmulx  42243  itgiccshift  42254  itgperiod  42255  dirkeritg  42377  dirkercncflem2  42379  dirkercncflem4  42381  fourierdlem16  42398  fourierdlem21  42403  fourierdlem22  42404  fourierdlem28  42410  fourierdlem42  42424  fourierdlem78  42459  fourierdlem81  42462  fourierdlem83  42464  fourierdlem84  42465  fourierdlem90  42471  fourierdlem93  42474  fourierdlem103  42484  fourierdlem104  42485  sge0resrnlem  42675  ismeannd  42739  0ome  42801  hoidmvlelem3  42869  hoidmvlelem4  42870  funcrngcsetc  44259  funcringcsetc  44296  rhmsubclem1  44347  rhmsubcALTVlem1  44365  aacllem  44892