Theorem reseq1d 5931

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

Syntax hints:   → wi 4   = wceq 1541   ↾ cres 5621

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-sb 2068  df-clab 2712  df-cleq 2725  df-clel 2808  df-rab 3397  df-in 3905  df-res 5631

This theorem is referenced by:  reseq12d  5933  fun2ssres  6531  funcnvres2  6566  fresin  6697  fresaunres2  6700  offres  7921  itunifval  10314  hsmex  10330  gruima  10700  fseq1p1m1  13500  ltweuz  13870  rlimres  15467  lo1res  15468  lo1resb  15473  rlimresb  15474  o1resb  15475  bitsf1ocnv  16357  fsets  17082  setsres  17091  setscom  17093  sscres  17732  resfval2  17802  estrres  18047  symgvalstruct  19311  gsumzres  19823  gsumzsplit  19841  gsum2dlem2  19885  dpjidcl  19974  pgpfaclem1  19997  funcrngcsetc  20557  funcringcsetc  20591  rhmsubclem1  20602  pwssplit2  20996  pwssplit3  20997  znle2  21492  phssip  21597  mamures  22313  ofco2  22367  mdetunilem9  22536  mdetmul  22539  smadiadetglem1  22587  smadiadetglem2  22588  tmdgsum  24011  tsmsval2  24046  tsmsres  24060  tsmssplit  24068  imasdsf1olem  24289  tmslem  24398  sranlm  24600  cmssmscld  25278  srabn  25288  cmscsscms  25301  mbflimsup  25595  dvres  25840  dvres3a  25843  dvmptresicc  25845  dvnres  25861  cpnres  25867  dvcmul  25875  dvcmulf  25876  dvcobr  25877  dvcobrOLD  25878  dvmptres3  25888  dvmptres2  25894  dvcnvlem  25908  dvlip2  25928  ftc2ditglem  25980  itgpowd  25985  aannenlem1  26264  eff1olem  26485  resqrtcn  26687  sqrtcn  26688  rlimcnp2  26904  jensenlem2  26926  ex-res  30423  rabfodom  32487  resf1o  32717  indf1ofs  32854  tocycfvres1  33086  tocycfvres2  33087  cycpmconjvlem  33117  cycpmconjslem2  33131  cyc3conja  33133  gsumind  33317  ply1gsumz  33566  lbsdiflsp0  33660  submatres  33840  zhmnrg  33999  carsggect  34352  fibp1  34435  actfunsnf1o  34638  cvmliftlem10  35359  cvmlift2lem6  35373  cvmlift2lem12  35379  satf  35418  poimirlem3  37683  ftc1anclem8  37760  ftc2nc  37762  cocnv  37785  cnpwstotbnd  37857  drngoi  38011  aks6d1c6lem2  42284  aks6d1c6lem4  42286  eldioph2  42879  dvsconst  44447  disjf1o  45312  cncfmptss  45711  limsupresuz  45825  liminfresuz  45906  itgsinexplem1  46076  itgcoscmulx  46091  itgiccshift  46102  itgperiod  46103  dirkeritg  46224  dirkercncflem2  46226  dirkercncflem4  46228  fourierdlem16  46245  fourierdlem21  46250  fourierdlem22  46251  fourierdlem28  46257  fourierdlem42  46271  fourierdlem78  46306  fourierdlem81  46309  fourierdlem83  46311  fourierdlem84  46312  fourierdlem90  46318  fourierdlem93  46321  fourierdlem103  46331  fourierdlem104  46332  sge0resrnlem  46525  ismeannd  46589  0ome  46651  hoidmvlelem3  46719  hoidmvlelem4  46720  rhmsubcALTVlem1  48405  aacllem  49926