Theorem reseq1i 5934

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 5932	. 2 ⊢ (𝐴 = 𝐵 → (𝐴 ↾ 𝐶) = (𝐵 ↾ 𝐶))
3	1, 2	ax-mp 5	1 ⊢ (𝐴 ↾ 𝐶) = (𝐵 ↾ 𝐶)

Syntax hints:   = wceq 1547   ↾ cres 5627

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2712

This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1787  df-sb 2074  df-clab 2719  df-cleq 2732  df-clel 2815  df-rab 3393  df-in 3897  df-res 5637

This theorem is referenced by:  reseq12i  5936  resindm  5989  resmpt  5996  resmpt3  5997  resmptf  5998  elimampt  6002  opabresid  6009  rescnvcnv  6162  coires1  6223  fnunres2  6605  fresaunres1  6707  fcoi1  6708  fninfp  7125  fvsnun1  7133  fvsnun2  7134  resoprab  7481  resmpo  7483  elimampo  7500  elrnmpores  7501  ofmres  7933  f1stres  7962  f2ndres  7963  df1st2  8044  df2nd2  8045  fsplitfpar  8064  dftpos2  8190  frrlem12  8244  tfr2a  8331  tfr2b  8332  rdgseg  8358  frsucmpt2  8376  seqomlem2  8387  seqomlem3  8388  seqomlem4  8389  domss2  9071  dffi3  9341  axdc  10441  fpwwe2lem12  10563  seqval  13972  hashgval  14293  hashinf  14295  submefmnd  18861  pgrpsubgsymg  19382  gsumzunsnd  19929  ablfac1b  20045  zzngim  21534  pmatcollpw3lem  22773  txflf  23996  xmsxmet2  24449  msmet2  24450  tmsxpsmopn  24527  isngp2  24587  subgnm  24623  tngngp2  24642  cnfldms  24765  msdcn  24832  oprpiece1res1  24943  oprpiece1res2  24944  isncvsngp  25141  cncms  25347  cnfldcusp  25349  reust  25373  minveclem3a  25419  dvreslem  25901  dvres2lem  25902  dvmptresicc  25908  dvcmulf  25937  mdegfval  26052  psercn  26416  abelth  26431  efcvx  26439  efifo  26536  dfrelog  26554  dvrelog  26626  dvlog  26640  efopnlem2  26646  dvatan  26924  dchrisumlem1  27477  noetasuplem2  27723  noetasuplem3  27724  noetasuplem4  27725  noetainflem2  27727  wlknwwlksnbij  29981  df1stres  32803  df2ndres  32804  padct  32817  ressplusf  33049  ressnm  33050  gsummpt2d  33137  cycpmrn  33231  tocyccntz  33232  cycpmconjslem2  33243  qusima  33498  qqhcn  34182  cnrrext  34201  rrhre  34212  esumcvg  34277  dya2icoseg2  34469  eulerpartgbij  34563  satf0  35607  neibastop2  36596  mptsnunlem  37707  icorempo  37720  poimirlem3  37997  mbfposadd  38041  ftc1anclem3  38069  dvasin  38078  dvacos  38079  prdsbnd2  38169  repwsmet  38208  rrnequiv  38209  inres2  38621  xrnres  38799  xrnres2  38800  xrnres3  38801  diophin  43228  eldioph4b  43263  dnnumch1  43496  aomclem6  43511  radcnvrat  44765  lhe4.4ex1a  44780  dvsid  44782  dvsef  44783  imassmpt  45713  elicores  45985  climresmpt  46109  dvcosre  46362  itgsinexplem1  46404  fourierdlem40  46597  fourierdlem57  46613  fourierdlem58  46614  fourierdlem62  46618  fourierdlem74  46630  fourierdlem75  46631  fourierdlem76  46632  fourierdlem80  46636  fourierdlem84  46640  fourierdlem85  46641  fourierdlem101  46657  fourierdlem102  46658  fourierdlem111  46667  fourierdlem114  46670  fouriersw  46681  fouriercn  46682  volicorescl  47003  fdmdifeqresdif  48840  tposresg  49375  tposrescnv  49376  rescofuf  49590  aacllem  50298