Theorem reseq1i 5979

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

This proof depends on syntax axioms:   = wceq 1570   ↾ cres 5668

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-ext 2738

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-sb 2100  df-clab 2745  df-cleq 2758  df-clel 2841  df-rab 3420  df-in 3915  df-res 5678

This theorem is used by:  reseq12i  5981  resindmOLD  6035  resmpt  6044  resmpt3  6045  resmptf  6046  elimampt  6050  opabresid  6057  rescnvcnv  6210  coires1  6271  fnunres2  6655  fresaunres1  6758  fcoi1  6759  fninfp  7179  fvsnun1  7187  fvsnun2  7188  resoprab  7541  resmpo  7543  elimampo  7560  elrnmpores  7561  ofmres  7990  f1stres  8019  f2ndres  8020  df1st2  8102  df2nd2  8103  fsplitfpar  8122  dftpos2  8248  frrlem12  8303  tfr2a  8391  tfr2b  8392  rdgseg  8418  frsucmpt2  8436  seqomlem2  8447  seqomlem3  8448  seqomlem4  8449  domss2  9134  dffi3  9401  axdc  10523  fpwwe2lem12  10645  seqval  14068  hashgval  14389  hashinf  14391  submefmnd  18985  pgrpsubgsymg  19510  gsumzunsnd  20057  ablfac1b  20173  zzngim  21739  pmatcollpw3lem  22977  txflf  24200  xmsxmet2  24653  msmet2  24654  tmsxpsmopn  24731  isngp2  24791  subgnm  24827  tngngp2  24846  cnfldms  24969  msdcn  25036  oprpiece1res1  25147  oprpiece1res2  25148  isncvsngp  25345  cncms  25551  cnfldcusp  25553  reust  25577  minveclem3a  25623  dvreslem  26105  dvres2lem  26106  dvmptresicc  26112  dvcmulf  26141  mdegfval  26256  psercn  26626  abelth  26641  efcvx  26649  efifo  26749  dfrelog  26767  dvrelog  26839  dvlog  26853  efopnlem2  26859  dvatan  27137  dchrisumlem1  27690  noetasuplem2  27935  noetasuplem3  27936  noetasuplem4  27937  noetainflem2  27939  wlknwwlksnbij  30274  df1stres  33086  df2ndres  33087  padct  33100  ressplusf  33314  ressnm  33315  gsummpt2d  33400  cycpmrn  33494  tocyccntz  33495  cycpmconjslem2  33506  qusima  33748  qqhcn  34412  cnrrext  34431  rrhre  34442  esumcvg  34507  dya2icoseg2  34699  eulerpartgbij  34793  satf0  35884  neibastop2  36912  mptsnunlem  38024  icorempo  38037  poimirlem3  38314  mbfposadd  38358  ftc1anclem3  38386  dvasin  38395  dvacos  38396  prdsbnd2  38486  repwsmet  38525  rrnequiv  38526  inres2  38936  xrnres  39114  xrnres2  39115  xrnres3  39116  diophin  43543  eldioph4b  43578  dnnumch1  43811  aomclem6  43826  radcnvrat  45064  lhe4.4ex1a  45079  dvsid  45081  dvsef  45082  imassmpt  46017  elicores  46289  climresmpt  46413  dvcosre  46666  itgsinexplem1  46708  fourierdlem40  46901  fourierdlem57  46917  fourierdlem58  46918  fourierdlem62  46922  fourierdlem74  46934  fourierdlem75  46935  fourierdlem76  46936  fourierdlem80  46940  fourierdlem84  46944  fourierdlem85  46945  fourierdlem101  46961  fourierdlem102  46962  fourierdlem111  46971  fourierdlem114  46974  fouriersw  46985  fouriercn  46986  volicorescl  47307  fdmdifeqresdif  49162  tposresg  49696  tposrescnv  49697  rescofuf  49911  aacllem  50661