Theorem reseq1i 6005

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

Syntax hints:   = wceq 1537   ↾ cres 5702

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-rab 3444  df-in 3983  df-res 5712

This theorem is referenced by:  reseq12i  6007  resindm  6059  resmpt  6066  resmpt3  6067  resmptf  6068  elimampt  6072  opabresid  6079  rescnvcnv  6235  coires1  6295  fnunres2  6692  fresaunres1  6794  fcoi1  6795  fninfp  7208  fvsnun1  7216  fvsnun2  7217  resoprab  7568  resmpo  7570  elimampo  7587  elrnmpores  7588  ofmres  8025  f1stres  8054  f2ndres  8055  df1st2  8139  df2nd2  8140  fsplitfpar  8159  dftpos2  8284  frrlem12  8338  wfrlem14OLD  8378  tfr2a  8451  tfr2b  8452  rdgseg  8478  frsucmpt2  8496  seqomlem2  8507  seqomlem3  8508  seqomlem4  8509  domss2  9202  dffi3  9500  fpwwe2lem12  10711  seqval  14063  hashgval  14382  hashinf  14384  submefmnd  18930  pgrpsubgsymg  19451  gsumzunsnd  19998  ablfac1b  20114  zzngim  21594  pmatcollpw3lem  22810  txflf  24035  xmsxmet2  24490  msmet2  24491  tmsxpsmopn  24571  isngp2  24631  subgnm  24667  tngngp2  24694  cnfldms  24817  msdcn  24882  oprpiece1res1  25001  oprpiece1res2  25002  isncvsngp  25202  cncms  25408  cnfldcusp  25410  reust  25434  minveclem3a  25480  dvreslem  25964  dvres2lem  25965  dvmptresicc  25971  dvcmulf  26002  mdegfval  26121  psercn  26488  abelth  26503  efcvx  26511  efifo  26607  dfrelog  26625  dvrelog  26697  dvlog  26711  efopnlem2  26717  dvatan  26996  dchrisumlem1  27551  noetasuplem2  27797  noetasuplem3  27798  noetasuplem4  27799  noetainflem2  27801  wlknwwlksnbij  29921  df1stres  32715  df2ndres  32716  padct  32733  ressplusf  32930  ressnm  32931  gsummpt2d  33032  cycpmrn  33136  tocyccntz  33137  cycpmconjslem2  33148  qusima  33401  qqhcn  33937  cnrrext  33956  rrhre  33967  esumcvg  34050  dya2icoseg2  34243  eulerpartgbij  34337  satf0  35340  neibastop2  36327  mptsnunlem  37304  icorempo  37317  poimirlem3  37583  mbfposadd  37627  ftc1anclem3  37655  dvasin  37664  dvacos  37665  prdsbnd2  37755  repwsmet  37794  rrnequiv  37795  inres2  38201  xrnres  38358  xrnres2  38359  xrnres3  38360  diophin  42728  eldioph4b  42767  dnnumch1  43001  aomclem6  43016  radcnvrat  44283  lhe4.4ex1a  44298  dvsid  44300  dvsef  44301  imassmpt  45172  elicores  45451  climresmpt  45580  dvcosre  45833  itgsinexplem1  45875  fourierdlem40  46068  fourierdlem57  46084  fourierdlem58  46085  fourierdlem62  46089  fourierdlem74  46101  fourierdlem75  46102  fourierdlem76  46103  fourierdlem80  46107  fourierdlem84  46111  fourierdlem85  46112  fourierdlem101  46128  fourierdlem102  46129  fourierdlem111  46138  fourierdlem114  46141  fouriersw  46152  fouriercn  46153  volicorescl  46474  fdmdifeqresdif  48066  aacllem  48895