Theorem reseq1d 5982

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

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

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 2148  ax-9 2156  ax-ext 2738

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-sb 2100  df-clab 2745  df-cleq 2758  df-clel 2841  df-rab 3420  df-in 3915  df-res 5678

This theorem is used by:  reseq12d  5984  fun2ssres  6588  funcnvres2  6623  fresin  6754  fresaunres2  6757  offres  7989  itunifval  10418  hsmex  10434  gruima  10805  fseq1p1m1  13645  ltweuz  14017  rlimres  15635  lo1res  15636  lo1resb  15641  rlimresb  15642  o1resb  15643  bitsf1ocnv  16527  fsets  17254  setsres  17263  setscom  17265  sscres  17905  resfval2  17975  estrres  18220  symgvalstruct  19498  gsumzres  20010  gsumzsplit  20028  gsum2dlem2  20072  dpjidcl  20161  pgpfaclem1  20184  funcrngcsetc  20776  funcringcsetc  20810  rhmsubclem1  20821  pwssplit2  21218  pwssplit3  21219  znle2  21740  phssip  21845  mamures  22591  ofco2  22645  mdetunilem9  22814  mdetmul  22817  smadiadetglem1  22865  smadiadetglem2  22866  tmdgsum  24289  tsmsval2  24324  tsmsres  24338  tsmssplit  24346  imasdsf1olem  24567  tmslem  24676  sranlm  24878  cmssmscld  25546  srabn  25556  cmscsscms  25569  mbflimsup  25862  dvres  26107  dvres3a  26110  dvmptresicc  26112  dvnres  26127  cpnres  26133  dvcmul  26140  dvcmulf  26141  dvcobr  26142  dvmptres3  26152  dvmptres2  26158  dvcnvlem  26172  dvlip2  26191  ftc2ditglem  26241  itgpowd  26246  aannenlem1  26528  eff1olem  26750  resqrtcn  26951  sqrtcn  26952  rlimcnp2  27168  jensenlem2  27189  ex-res  30829  rabfodom  32888  padct  33100  resf1o  33112  indf1ofs  33223  tocycfvres1  33461  tocycfvres2  33462  cycpmconjvlem  33492  cycpmconjslem2  33506  cyc3conja  33508  gsumind  33696  ply1gsumz  33920  evlextv  33963  lbsdiflsp0  34047  submatres  34227  zhmnrg  34386  carsggect  34740  fibp1  34823  actfunsnf1o  35023  cvmliftlem10  35807  cvmlift2lem6  35821  cvmlift2lem12  35827  satf  35866  poimirlem3  38315  ftc1anclem8  38392  ftc2nc  38394  cocnv  38417  cnpwstotbnd  38489  drngoi  38643  aks6d1c6lem2  42979  aks6d1c6lem4  42981  eldioph2  43534  dvsconst  45081  disjf1o  45950  cncfmptss  46344  limsupresuz  46458  liminfresuz  46539  itgsinexplem1  46709  itgcoscmulx  46724  itgiccshift  46735  itgperiod  46736  dirkeritg  46857  dirkercncflem2  46859  dirkercncflem4  46861  fourierdlem16  46878  fourierdlem21  46883  fourierdlem22  46884  fourierdlem28  46890  fourierdlem42  46904  fourierdlem78  46939  fourierdlem81  46942  fourierdlem83  46944  fourierdlem84  46945  fourierdlem90  46951  fourierdlem93  46954  fourierdlem103  46964  fourierdlem104  46965  sge0resrnlem  47158  ismeannd  47222  0ome  47284  hoidmvlelem3  47352  hoidmvlelem4  47353  rhmsubcALTVlem1  49087  aacllem  50662