Theorem reseq1i 5981

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

Syntax hints:   = wceq 1533   ↾ cres 5680

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-ext 2696

This theorem depends on definitions:  df-bi 206  df-an 395  df-ex 1774  df-sb 2060  df-clab 2703  df-cleq 2717  df-clel 2802  df-rab 3419  df-in 3951  df-res 5690

This theorem is referenced by:  reseq12i  5983  resindm  6035  resmpt  6042  resmpt3  6043  resmptf  6044  opabresid  6054  rescnvcnv  6210  coires1  6270  fnunres2  6668  fresaunres1  6770  fcoi1  6771  fninfp  7183  fvsnun1  7191  fvsnun2  7192  resoprab  7538  resmpo  7540  elimampo  7558  elrnmpores  7559  ofmres  7989  f1stres  8018  f2ndres  8019  df1st2  8103  df2nd2  8104  fsplitfpar  8123  dftpos2  8249  frrlem12  8303  wfrlem14OLD  8343  tfr2a  8416  tfr2b  8417  rdgseg  8443  frsucmpt2  8461  seqomlem2  8472  seqomlem3  8473  seqomlem4  8474  domss2  9164  dffi3  9461  fpwwe2lem12  10672  seqval  14018  hashgval  14336  hashinf  14338  submefmnd  18871  pgrpsubgsymg  19393  gsumzunsnd  19940  ablfac1b  20056  zzngim  21520  pmatcollpw3lem  22746  txflf  23971  xmsxmet2  24426  msmet2  24427  tmsxpsmopn  24507  isngp2  24567  subgnm  24603  tngngp2  24630  cnfldms  24753  msdcn  24818  oprpiece1res1  24937  oprpiece1res2  24938  isncvsngp  25138  cncms  25344  cnfldcusp  25346  reust  25370  minveclem3a  25416  dvreslem  25899  dvres2lem  25900  dvmptresicc  25906  dvcmulf  25937  mdegfval  26059  psercn  26425  abelth  26440  efcvx  26448  efifo  26543  dfrelog  26561  dvrelog  26633  dvlog  26647  efopnlem2  26653  dvatan  26932  dchrisumlem1  27487  noetasuplem2  27733  noetasuplem3  27734  noetasuplem4  27735  noetainflem2  27737  wlknwwlksnbij  29791  elimampt  32524  df1stres  32585  df2ndres  32586  padct  32603  ressplusf  32794  ressnm  32795  gsummpt2d  32874  cycpmrn  32977  tocyccntz  32978  cycpmconjslem2  32989  qusima  33241  qqhcn  33743  cnrrext  33762  rrhre  33773  esumcvg  33856  dya2icoseg2  34049  eulerpartgbij  34143  satf0  35133  neibastop2  35996  mptsnunlem  36968  icorempo  36981  poimirlem3  37247  mbfposadd  37291  ftc1anclem3  37319  dvasin  37328  dvacos  37329  prdsbnd2  37419  repwsmet  37458  rrnequiv  37459  inres2  37867  xrnres  38024  xrnres2  38025  xrnres3  38026  diophin  42339  eldioph4b  42378  dnnumch1  42615  aomclem6  42630  radcnvrat  43898  lhe4.4ex1a  43913  dvsid  43915  dvsef  43916  imassmpt  44782  elicores  45061  climresmpt  45190  dvcosre  45443  itgsinexplem1  45485  fourierdlem40  45678  fourierdlem57  45694  fourierdlem58  45695  fourierdlem62  45699  fourierdlem74  45711  fourierdlem75  45712  fourierdlem76  45713  fourierdlem80  45717  fourierdlem84  45721  fourierdlem85  45722  fourierdlem101  45738  fourierdlem102  45739  fourierdlem111  45748  fourierdlem114  45751  fouriersw  45762  fouriercn  45763  volicorescl  46084  fdmdifeqresdif  47596  aacllem  48425