Theorem reseq1i 5814

Description: Equality inference for restrictions. (Contributed by NM, 21-Oct-2014.)

Hypothesis

Ref	Expression
reseqi.1	⊢ 𝐴 = 𝐵

Assertion

Ref	Expression
reseq1i	⊢ (𝐴 ↾ 𝐶) = (𝐵 ↾ 𝐶)

Proof of Theorem reseq1i

Step	Hyp	Ref	Expression
1		reseqi.1	. 2 ⊢ 𝐴 = 𝐵
2		reseq1 5812	. 2 ⊢ (𝐴 = 𝐵 → (𝐴 ↾ 𝐶) = (𝐵 ↾ 𝐶))
3	1, 2	ax-mp 5	1 ⊢ (𝐴 ↾ 𝐶) = (𝐵 ↾ 𝐶)

Syntax hints:   = wceq 1538   ↾ cres 5521

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-ext 2770

This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-sb 2070  df-clab 2777  df-cleq 2791  df-clel 2870  df-rab 3115  df-in 3888  df-res 5531

This theorem is referenced by:  reseq12i  5816  resindm  5867  resmpt  5872  resmpt3  5873  resmptf  5874  opabresid  5884  opabresidOLD  5886  rescnvcnv  6028  coires1  6084  fresaunres1  6525  fcoi1  6526  fninfp  6913  fvsnun1  6921  fvsnun2  6922  resoprab  7249  resmpo  7251  elrnmpores  7267  ofmres  7667  f1stres  7695  f2ndres  7696  df1st2  7776  df2nd2  7777  fsplitfpar  7797  dftpos2  7892  wfrlem14  7951  tfr2a  8014  tfr2b  8015  rdgseg  8041  frsucmpt2w  8058  frsucmpt2  8059  seqomlem2  8070  seqomlem3  8071  seqomlem4  8072  domss2  8660  dffi3  8879  fpwwe2lem13  10053  seqval  13375  hashgval  13689  hashinf  13691  submefmnd  18052  pgrpsubgsymg  18529  gsumzunsnd  19069  ablfac1b  19185  zzngim  20244  pmatcollpw3lem  21388  txflf  22611  xmsxmet2  23066  msmet2  23067  tmsxpsmopn  23144  isngp2  23203  subgnm  23239  tngngp2  23258  cnfldms  23381  msdcn  23446  oprpiece1res1  23556  oprpiece1res2  23557  isncvsngp  23754  cncms  23959  cnfldcusp  23961  reust  23985  minveclem3a  24031  dvreslem  24512  dvres2lem  24513  dvmptresicc  24519  dvcmulf  24548  mdegfval  24663  psercn  25021  abelth  25036  efcvx  25044  efifo  25139  dfrelog  25157  dvrelog  25228  dvlog  25242  efopnlem2  25248  dvatan  25521  dchrisumlem1  26073  wlknwwlksnbij  27674  elimampt  30397  fnunres2  30441  df1stres  30463  df2ndres  30464  padct  30481  ressplusf  30663  ressnm  30664  gsummpt2d  30734  cycpmrn  30835  tocyccntz  30836  cycpmconjslem2  30847  qqhcn  31342  cnrrext  31361  rrhre  31372  esumcvg  31455  dya2icoseg2  31646  eulerpartgbij  31740  satf0  32732  trpred0  33188  frrlem12  33247  noetalem2  33331  noetalem3  33332  neibastop2  33822  mptsnunlem  34755  icorempo  34768  poimirlem3  35060  mbfposadd  35104  ftc1anclem3  35132  dvasin  35141  dvacos  35142  prdsbnd2  35233  repwsmet  35272  rrnequiv  35273  inres2  35666  xrnres  35810  xrnres2  35811  xrnres3  35812  diophin  39713  eldioph4b  39752  dnnumch1  39988  aomclem6  40003  radcnvrat  41018  lhe4.4ex1a  41033  dvsid  41035  dvsef  41036  imassmpt  41902  elicores  42170  climresmpt  42301  dvcosre  42554  itgsinexplem1  42596  fourierdlem40  42789  fourierdlem57  42805  fourierdlem58  42806  fourierdlem62  42810  fourierdlem74  42822  fourierdlem75  42823  fourierdlem76  42824  fourierdlem80  42828  fourierdlem84  42832  fourierdlem85  42833  fourierdlem101  42849  fourierdlem102  42850  fourierdlem111  42859  fourierdlem114  42862  fouriersw  42873  fouriercn  42874  volicorescl  43192  fdmdifeqresdif  44743  aacllem  45329