Theorem reseq1d 5975

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

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

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 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2734

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-sb 2100  df-clab 2741  df-cleq 2754  df-clel 2837  df-rab 3415  df-in 3909  df-res 5671

This theorem is used by:  reseq12d  5977  fun2ssres  6582  funcnvres2  6617  fresin  6748  fresaunres2  6751  offres  7984  itunifval  10422  hsmex  10438  gruima  10815  fseq1p1m1  13657  ltweuz  14029  rlimres  15649  lo1res  15650  lo1resb  15655  rlimresb  15656  o1resb  15657  bitsf1ocnv  16540  fsets  17267  setsres  17276  setscom  17278  sscres  17918  resfval2  17988  estrres  18233  symgvalstruct  19530  gsumzres  20042  gsumzsplit  20060  gsum2dlem2  20104  dpjidcl  20193  pgpfaclem1  20216  funcrngcsetc  20808  funcringcsetc  20842  rhmsubclem1  20853  pwssplit2  21250  pwssplit3  21251  znle2  21772  phssip  21877  mamures  22625  ofco2  22679  mdetunilem9  22848  mdetmul  22851  smadiadetglem1  22899  smadiadetglem2  22900  tmdgsum  24327  tsmsval2  24362  tsmsres  24376  tsmssplit  24384  imasdsf1olem  24605  tmslem  24714  sranlm  24916  cmssmscld  25584  srabn  25594  cmscsscms  25607  mbflimsup  25900  dvres  26145  dvres3a  26148  dvmptresicc  26150  dvnres  26165  cpnres  26171  dvcmul  26178  dvcmulf  26179  dvcobr  26180  dvmptres3  26190  dvmptres2  26196  dvcnvlem  26210  dvlip2  26229  ftc2ditglem  26279  itgpowd  26284  aannenlem1  26571  eff1olem  26793  resqrtcn  26994  sqrtcn  26995  rlimcnp2  27211  jensenlem2  27232  ex-res  30929  rabfodom  32988  padct  33197  resf1o  33209  indf1ofs  33320  tocycfvres1  33558  tocycfvres2  33559  cycpmconjvlem  33589  cycpmconjslem2  33603  cyc3conja  33605  gsumind  33793  ply1gsumz  34017  evlextv  34060  lbsdiflsp0  34144  submatres  34324  zhmnrg  34483  carsggect  34837  fibp1  34920  actfunsnf1o  35120  cvmliftlem10  35881  cvmlift2lem6  35895  cvmlift2lem12  35901  satf  35940  poimirlem3  38380  ftc1anclem8  38457  ftc2nc  38459  cocnv  38483  cnpwstotbnd  38555  drngoi  38709  aks6d1c6lem2  43045  aks6d1c6lem4  43047  eldioph2  43615  dvsconst  45162  disjf1o  46031  cncfmptss  46425  limsupresuz  46539  liminfresuz  46620  itgsinexplem1  46790  itgcoscmulx  46805  itgiccshift  46816  itgperiod  46817  dirkeritg  46938  dirkercncflem2  46940  dirkercncflem4  46942  fourierdlem16  46959  fourierdlem21  46964  fourierdlem22  46965  fourierdlem28  46971  fourierdlem42  46985  fourierdlem78  47020  fourierdlem81  47023  fourierdlem83  47025  fourierdlem84  47026  fourierdlem90  47032  fourierdlem93  47035  fourierdlem103  47045  fourierdlem104  47046  sge0resrnlem  47239  ismeannd  47303  0ome  47365  hoidmvlelem3  47433  hoidmvlelem4  47434  rhmsubcALTVlem1  49204  aacllem  50780