Theorem reseq1i 5967

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

Syntax hints:   = wceq 1540   ↾ cres 5661

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-sb 2066  df-clab 2715  df-cleq 2728  df-clel 2810  df-rab 3421  df-in 3938  df-res 5671

This theorem is referenced by:  reseq12i  5969  resindm  6022  resmpt  6029  resmpt3  6030  resmptf  6031  elimampt  6035  opabresid  6042  rescnvcnv  6198  coires1  6258  fnunres2  6656  fresaunres1  6756  fcoi1  6757  fninfp  7171  fvsnun1  7179  fvsnun2  7180  resoprab  7530  resmpo  7532  elimampo  7549  elrnmpores  7550  ofmres  7988  f1stres  8017  f2ndres  8018  df1st2  8102  df2nd2  8103  fsplitfpar  8122  dftpos2  8247  frrlem12  8301  wfrlem14OLD  8341  tfr2a  8414  tfr2b  8415  rdgseg  8441  frsucmpt2  8459  seqomlem2  8470  seqomlem3  8471  seqomlem4  8472  domss2  9155  dffi3  9448  axdc  10540  fpwwe2lem12  10661  seqval  14035  hashgval  14356  hashinf  14358  submefmnd  18878  pgrpsubgsymg  19395  gsumzunsnd  19942  ablfac1b  20058  zzngim  21518  pmatcollpw3lem  22726  txflf  23949  xmsxmet2  24403  msmet2  24404  tmsxpsmopn  24481  isngp2  24541  subgnm  24577  tngngp2  24596  cnfldms  24719  msdcn  24786  oprpiece1res1  24905  oprpiece1res2  24906  isncvsngp  25106  cncms  25312  cnfldcusp  25314  reust  25338  minveclem3a  25384  dvreslem  25867  dvres2lem  25868  dvmptresicc  25874  dvcmulf  25905  mdegfval  26024  psercn  26393  abelth  26408  efcvx  26416  efifo  26513  dfrelog  26531  dvrelog  26603  dvlog  26617  efopnlem2  26623  dvatan  26902  dchrisumlem1  27457  noetasuplem2  27703  noetasuplem3  27704  noetasuplem4  27705  noetainflem2  27707  wlknwwlksnbij  29875  df1stres  32686  df2ndres  32687  padct  32702  ressplusf  32944  ressnm  32945  gsummpt2d  33048  cycpmrn  33159  tocyccntz  33160  cycpmconjslem2  33171  qusima  33428  qqhcn  34027  cnrrext  34046  rrhre  34057  esumcvg  34122  dya2icoseg2  34315  eulerpartgbij  34409  satf0  35399  neibastop2  36384  mptsnunlem  37361  icorempo  37374  poimirlem3  37652  mbfposadd  37696  ftc1anclem3  37724  dvasin  37733  dvacos  37734  prdsbnd2  37824  repwsmet  37863  rrnequiv  37864  inres2  38269  xrnres  38425  xrnres2  38426  xrnres3  38427  diophin  42770  eldioph4b  42809  dnnumch1  43043  aomclem6  43058  radcnvrat  44313  lhe4.4ex1a  44328  dvsid  44330  dvsef  44331  imassmpt  45266  elicores  45542  climresmpt  45668  dvcosre  45921  itgsinexplem1  45963  fourierdlem40  46156  fourierdlem57  46172  fourierdlem58  46173  fourierdlem62  46177  fourierdlem74  46189  fourierdlem75  46190  fourierdlem76  46191  fourierdlem80  46195  fourierdlem84  46199  fourierdlem85  46200  fourierdlem101  46216  fourierdlem102  46217  fourierdlem111  46226  fourierdlem114  46229  fouriersw  46240  fouriercn  46241  volicorescl  46562  fdmdifeqresdif  48297  tposresg  48833  tposrescnv  48834  rescofuf  49036  aacllem  49645