Theorem reseq1i 5942

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

Syntax hints:   = wceq 1542   ↾ cres 5634

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 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-rab 3402  df-in 3910  df-res 5644

This theorem is referenced by:  reseq12i  5944  resindm  5997  resmpt  6004  resmpt3  6005  resmptf  6006  elimampt  6010  opabresid  6017  rescnvcnv  6170  coires1  6231  fnunres2  6613  fresaunres1  6715  fcoi1  6716  fninfp  7130  fvsnun1  7138  fvsnun2  7139  resoprab  7486  resmpo  7488  elimampo  7505  elrnmpores  7506  ofmres  7938  f1stres  7967  f2ndres  7968  df1st2  8050  df2nd2  8051  fsplitfpar  8070  dftpos2  8195  frrlem12  8249  tfr2a  8336  tfr2b  8337  rdgseg  8363  frsucmpt2  8381  seqomlem2  8392  seqomlem3  8393  seqomlem4  8394  domss2  9076  dffi3  9346  axdc  10443  fpwwe2lem12  10565  seqval  13947  hashgval  14268  hashinf  14270  submefmnd  18832  pgrpsubgsymg  19350  gsumzunsnd  19897  ablfac1b  20013  zzngim  21519  pmatcollpw3lem  22739  txflf  23962  xmsxmet2  24415  msmet2  24416  tmsxpsmopn  24493  isngp2  24553  subgnm  24589  tngngp2  24608  cnfldms  24731  msdcn  24798  oprpiece1res1  24917  oprpiece1res2  24918  isncvsngp  25117  cncms  25323  cnfldcusp  25325  reust  25349  minveclem3a  25395  dvreslem  25878  dvres2lem  25879  dvmptresicc  25885  dvcmulf  25916  mdegfval  26035  psercn  26404  abelth  26419  efcvx  26427  efifo  26524  dfrelog  26542  dvrelog  26614  dvlog  26628  efopnlem2  26634  dvatan  26913  dchrisumlem1  27468  noetasuplem2  27714  noetasuplem3  27715  noetasuplem4  27716  noetainflem2  27718  wlknwwlksnbij  29973  df1stres  32793  df2ndres  32794  padct  32807  ressplusf  33055  ressnm  33056  gsummpt2d  33142  cycpmrn  33236  tocyccntz  33237  cycpmconjslem2  33248  qusima  33500  qqhcn  34168  cnrrext  34187  rrhre  34198  esumcvg  34263  dya2icoseg2  34455  eulerpartgbij  34549  satf0  35585  neibastop2  36574  mptsnunlem  37587  icorempo  37600  poimirlem3  37868  mbfposadd  37912  ftc1anclem3  37940  dvasin  37949  dvacos  37950  prdsbnd2  38040  repwsmet  38079  rrnequiv  38080  inres2  38492  xrnres  38670  xrnres2  38671  xrnres3  38672  diophin  43123  eldioph4b  43162  dnnumch1  43395  aomclem6  43410  radcnvrat  44664  lhe4.4ex1a  44679  dvsid  44681  dvsef  44682  imassmpt  45614  elicores  45887  climresmpt  46011  dvcosre  46264  itgsinexplem1  46306  fourierdlem40  46499  fourierdlem57  46515  fourierdlem58  46516  fourierdlem62  46520  fourierdlem74  46532  fourierdlem75  46533  fourierdlem76  46534  fourierdlem80  46538  fourierdlem84  46542  fourierdlem85  46543  fourierdlem101  46559  fourierdlem102  46560  fourierdlem111  46569  fourierdlem114  46572  fouriersw  46583  fouriercn  46584  volicorescl  46905  fdmdifeqresdif  48696  tposresg  49231  tposrescnv  49232  rescofuf  49446  aacllem  50154