Theorem reseq1d 5981

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

This proof depends on syntax axioms:   → wi 4   = wceq 1570   ↾ cres 5658

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-sb 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-rab 3417  df-in 4094  df-res 5668

This theorem is used by:  reseq12d  5983  fun2ssres  6608  funcnvres2  6645  fresin  6776  fresaunres2  6779  offres  8022  itunifval  10524  hsmex  10540  gruima  10917  fseq1p1m1  13762  ltweuz  14134  rlimres  15757  lo1res  15758  lo1resb  15763  rlimresb  15764  o1resb  15765  bitsf1ocnv  16646  fsets  17379  setsres  17388  setscom  17390  sscres  18030  resfval2  18100  estrres  18345  symgvalstruct  19644  gsumzres  20156  gsumzsplit  20174  gsum2dlem2  20218  dpjidcl  20307  pgpfaclem1  20330  funcrngcsetc  20925  funcringcsetc  20959  rhmsubclem1  20970  pwssplit2  21368  pwssplit3  21369  znle2  21892  phssip  21997  mamures  22745  ofco2  22799  mdetunilem9  22968  mdetmul  22971  smadiadetglem1  23019  smadiadetglem2  23020  tmdgsum  24447  tsmsval2  24482  tsmsres  24496  tsmssplit  24504  imasdsf1olem  24725  tmslem  24834  sranlm  25036  cmssmscld  25704  srabn  25714  cmscsscms  25727  mbflimsup  26020  dvres  26264  dvres3a  26267  dvmptresicc  26269  dvnres  26284  cpnres  26290  dvcmul  26297  dvcmulf  26298  dvcobr  26299  dvmptres3  26309  dvmptres2  26315  dvcnvlem  26329  dvlip2  26348  ftc2ditglem  26398  itgpowd  26403  aannenlem1  26688  eff1olem  26909  resqrtcn  27110  sqrtcn  27111  rlimcnp2  27327  jensenlem2  27348  ex-res  31075  rabfodom  33176  padct  33384  resf1o  33395  indf1ofs  33506  tocycfvres1  33747  tocycfvres2  33748  cycpmconjvlem  33778  cycpmconjslem2  33792  cyc3conja  33794  gsumind  33990  ply1gsumz  34214  evlextv  34257  lbsdiflsp0  34341  submatres  34521  zhmnrg  34680  carsggect  35033  fibp1  35116  actfunsnf1o  35316  cvmliftlem10  36239  cvmlift2lem6  36253  cvmlift2lem12  36259  satf  36298  poimirlem3  38746  ftc1anclem8  38823  ftc2nc  38825  cocnv  38864  cnpwstotbnd  38934  drngoi  39088  aks6d1c6lem2  43424  aks6d1c6lem4  43426  eldioph2  43977  dvsconst  45517  disjf1o  46421  cncfmptss  46814  limsupresuz  46928  liminfresuz  47009  itgsinexplem1  47179  itgcoscmulx  47194  itgiccshift  47205  itgperiod  47206  dirkeritg  47327  dirkercncflem2  47329  dirkercncflem4  47331  fourierdlem16  47348  fourierdlem21  47353  fourierdlem22  47354  fourierdlem28  47360  fourierdlem42  47374  fourierdlem78  47409  fourierdlem81  47412  fourierdlem83  47414  fourierdlem84  47415  fourierdlem90  47421  fourierdlem93  47424  fourierdlem103  47434  fourierdlem104  47435  sge0resrnlem  47628  ismeannd  47692  0ome  47754  hoidmvlelem3  47822  hoidmvlelem4  47823  rhmsubcALTVlem1  49593  aacllem  51251