Theorem reseq1i 5965

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

Syntax hints:   = wceq 1563   ↾ cres 5654

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1818  ax-4 1832  ax-5 1933  ax-6 1990  ax-7 2031  ax-8 2147  ax-9 2155  ax-ext 2737

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1803  df-sb 2094  df-clab 2744  df-cleq 2757  df-clel 2840  df-rab 3418  df-in 3914  df-res 5664

This theorem is referenced by:  reseq12i  5967  resindmOLD  6021  resmpt  6030  resmpt3  6031  resmptf  6032  elimampt  6036  opabresid  6043  rescnvcnv  6195  coires1  6256  fnunres2  6638  fresaunres1  6741  fcoi1  6742  fninfp  7162  fvsnun1  7170  fvsnun2  7171  resoprab  7518  resmpo  7520  elimampo  7537  elrnmpores  7538  ofmres  7969  f1stres  7998  f2ndres  7999  df1st2  8081  df2nd2  8082  fsplitfpar  8101  dftpos2  8227  frrlem12  8282  tfr2a  8370  tfr2b  8371  rdgseg  8397  frsucmpt2  8415  seqomlem2  8426  seqomlem3  8427  seqomlem4  8428  domss2  9112  dffi3  9379  axdc  10493  fpwwe2lem12  10615  seqval  14039  hashgval  14360  hashinf  14362  submefmnd  18944  pgrpsubgsymg  19470  gsumzunsnd  20017  ablfac1b  20133  zzngim  21662  pmatcollpw3lem  22901  txflf  24124  xmsxmet2  24577  msmet2  24578  tmsxpsmopn  24655  isngp2  24715  subgnm  24751  tngngp2  24770  cnfldms  24893  msdcn  24960  oprpiece1res1  25071  oprpiece1res2  25072  isncvsngp  25269  cncms  25475  cnfldcusp  25477  reust  25501  minveclem3a  25547  dvreslem  26029  dvres2lem  26030  dvmptresicc  26036  dvcmulf  26065  mdegfval  26180  psercn  26547  abelth  26562  efcvx  26570  efifo  26670  dfrelog  26688  dvrelog  26760  dvlog  26774  efopnlem2  26780  dvatan  27058  dchrisumlem1  27611  noetasuplem2  27856  noetasuplem3  27857  noetasuplem4  27858  noetainflem2  27860  wlknwwlksnbij  30146  df1stres  32961  df2ndres  32962  padct  32975  ressplusf  33196  ressnm  33197  gsummpt2d  33282  cycpmrn  33376  tocyccntz  33377  cycpmconjslem2  33388  qusima  33633  qqhcn  34298  cnrrext  34317  rrhre  34328  esumcvg  34393  dya2icoseg2  34585  eulerpartgbij  34679  satf0  35735  neibastop2  36734  mptsnunlem  37844  icorempo  37857  poimirlem3  38134  mbfposadd  38178  ftc1anclem3  38206  dvasin  38215  dvacos  38216  prdsbnd2  38306  repwsmet  38345  rrnequiv  38346  inres2  38758  xrnres  38936  xrnres2  38937  xrnres3  38938  diophin  43365  eldioph4b  43400  dnnumch1  43633  aomclem6  43648  radcnvrat  44888  lhe4.4ex1a  44903  dvsid  44905  dvsef  44906  imassmpt  45835  elicores  46107  climresmpt  46231  dvcosre  46484  itgsinexplem1  46526  fourierdlem40  46719  fourierdlem57  46735  fourierdlem58  46736  fourierdlem62  46740  fourierdlem74  46752  fourierdlem75  46753  fourierdlem76  46754  fourierdlem80  46758  fourierdlem84  46762  fourierdlem85  46763  fourierdlem101  46779  fourierdlem102  46780  fourierdlem111  46789  fourierdlem114  46792  fouriersw  46803  fouriercn  46804  volicorescl  47125  fdmdifeqresdif  48973  tposresg  49507  tposrescnv  49508  rescofuf  49722  aacllem  50430