Theorem reseq1i 5851

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

Syntax hints:   = wceq 1537   ↾ cres 5559

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-ext 2795

This theorem depends on definitions:  df-bi 209  df-an 399  df-ex 1781  df-sb 2070  df-clab 2802  df-cleq 2816  df-clel 2895  df-rab 3149  df-in 3945  df-res 5569

This theorem is referenced by:  reseq12i  5853  resindm  5902  resmpt  5907  resmpt3  5908  resmptf  5909  opabresid  5919  opabresidOLD  5921  rescnvcnv  6063  coires1  6119  fresaunres1  6553  fcoi1  6554  fninfp  6938  fvsnun1  6946  fvsnun2  6947  resoprab  7272  resmpo  7274  elrnmpores  7290  ofmres  7687  f1stres  7715  f2ndres  7716  df1st2  7795  df2nd2  7796  fsplitfpar  7816  dftpos2  7911  wfrlem14  7970  tfr2a  8033  tfr2b  8034  rdgseg  8060  frsucmpt2w  8077  frsucmpt2  8078  seqomlem2  8089  seqomlem3  8090  seqomlem4  8091  domss2  8678  dffi3  8897  fpwwe2lem13  10066  seqval  13383  hashgval  13696  hashinf  13698  submefmnd  18062  pgrpsubgsymg  18539  gsumzunsnd  19078  ablfac1b  19194  zzngim  20701  pmatcollpw3lem  21393  txflf  22616  xmsxmet2  23071  msmet2  23072  tmsxpsmopn  23149  isngp2  23208  subgnm  23244  tngngp2  23263  cnfldms  23386  msdcn  23451  oprpiece1res1  23557  oprpiece1res2  23558  isncvsngp  23755  cncms  23960  cnfldcusp  23962  reust  23986  minveclem3a  24032  dvreslem  24509  dvres2lem  24510  dvcmulf  24544  mdegfval  24658  psercn  25016  abelth  25031  efcvx  25039  efifo  25133  dfrelog  25151  dvrelog  25222  dvlog  25236  efopnlem2  25242  dvatan  25515  dchrisumlem1  26067  wlknwwlksnbij  27668  elimampt  30385  fnunres2  30426  df1stres  30441  df2ndres  30442  padct  30457  ressplusf  30639  ressnm  30640  gsummpt2d  30689  cycpmrn  30787  tocyccntz  30788  cycpmconjslem2  30799  qqhcn  31234  cnrrext  31253  rrhre  31264  esumcvg  31347  dya2icoseg2  31538  eulerpartgbij  31632  satf0  32621  trpred0  33077  frrlem12  33136  noetalem2  33220  noetalem3  33221  neibastop2  33711  mptsnunlem  34621  icorempo  34634  poimirlem3  34897  mbfposadd  34941  ftc1anclem3  34971  dvasin  34980  dvacos  34981  prdsbnd2  35075  repwsmet  35114  rrnequiv  35115  inres2  35508  xrnres  35652  xrnres2  35653  xrnres3  35654  diophin  39376  eldioph4b  39415  dnnumch1  39651  aomclem6  39666  radcnvrat  40653  lhe4.4ex1a  40668  dvsid  40670  dvsef  40671  imassmpt  41544  elicores  41816  climresmpt  41947  dvcosre  42203  dvmptresicc  42211  itgsinexplem1  42246  fourierdlem40  42439  fourierdlem57  42455  fourierdlem58  42456  fourierdlem62  42460  fourierdlem74  42472  fourierdlem75  42473  fourierdlem76  42474  fourierdlem80  42478  fourierdlem84  42482  fourierdlem85  42483  fourierdlem101  42499  fourierdlem102  42500  fourierdlem111  42509  fourierdlem114  42512  fouriersw  42523  fouriercn  42524  volicorescl  42842  fdmdifeqresdif  44397  aacllem  44909