Theorem reseq1d 5890

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

Syntax hints:   → wi 4   = wceq 1539   ↾ cres 5591

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1783  df-sb 2068  df-clab 2716  df-cleq 2730  df-clel 2816  df-rab 3073  df-in 3894  df-res 5601

This theorem is referenced by:  reseq12d  5892  fun2ssres  6479  funcnvres2  6514  fresin  6643  fresaunres2  6646  offres  7826  itunifval  10172  hsmex  10188  gruima  10558  fseq1p1m1  13330  ltweuz  13681  rlimres  15267  lo1res  15268  lo1resb  15273  rlimresb  15274  o1resb  15275  bitsf1ocnv  16151  fsets  16870  setsres  16879  setscom  16881  sscres  17535  resfval2  17608  estrres  17856  symgvalstruct  19004  symgvalstructOLD  19005  gsumzres  19510  gsumzsplit  19528  gsum2dlem2  19572  dpjidcl  19661  pgpfaclem1  19684  pwssplit2  20322  pwssplit3  20323  znle2  20761  phssip  20863  mamures  21539  ofco2  21600  mdetunilem9  21769  mdetmul  21772  smadiadetglem1  21820  smadiadetglem2  21821  tmdgsum  23246  tsmsval2  23281  tsmsres  23295  tsmssplit  23303  imasdsf1olem  23526  tmslem  23637  tmslemOLD  23638  sranlm  23848  cmssmscld  24514  srabn  24524  cmscsscms  24537  mbflimsup  24830  dvres  25075  dvres3a  25078  dvmptresicc  25080  dvnres  25095  cpnres  25101  dvcmul  25108  dvcmulf  25109  dvcobr  25110  dvmptres3  25120  dvmptres2  25126  dvcnvlem  25140  dvlip2  25159  ftc2ditglem  25209  itgpowd  25214  aannenlem1  25488  eff1olem  25704  resqrtcn  25902  sqrtcn  25903  rlimcnp2  26116  jensenlem2  26137  ex-res  28805  rabfodom  30851  resf1o  31065  tocycfvres1  31377  tocycfvres2  31378  cycpmconjvlem  31408  cycpmconjslem2  31422  cyc3conja  31424  lbsdiflsp0  31707  submatres  31756  zhmnrg  31917  indf1ofs  31994  carsggect  32285  fibp1  32368  actfunsnf1o  32584  cvmliftlem10  33256  cvmlift2lem6  33270  cvmlift2lem12  33276  satf  33315  poimirlem3  35780  ftc1anclem8  35857  ftc2nc  35859  cocnv  35883  cnpwstotbnd  35955  drngoi  36109  eldioph2  40584  dvsconst  41948  disjf1o  42729  cncfmptss  43128  limsupresuz  43244  liminfresuz  43325  itgsinexplem1  43495  itgcoscmulx  43510  itgiccshift  43521  itgperiod  43522  dirkeritg  43643  dirkercncflem2  43645  dirkercncflem4  43647  fourierdlem16  43664  fourierdlem21  43669  fourierdlem22  43670  fourierdlem28  43676  fourierdlem42  43690  fourierdlem78  43725  fourierdlem81  43728  fourierdlem83  43730  fourierdlem84  43731  fourierdlem90  43737  fourierdlem93  43740  fourierdlem103  43750  fourierdlem104  43751  sge0resrnlem  43941  ismeannd  44005  0ome  44067  hoidmvlelem3  44135  hoidmvlelem4  44136  funcrngcsetc  45556  funcringcsetc  45593  rhmsubclem1  45644  rhmsubcALTVlem1  45662  aacllem  46505