Theorem reseq1i 5849

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

Syntax hints:   = wceq 1537   ↾ cres 5557

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-ext 2793

This theorem depends on definitions:  df-bi 209  df-an 399  df-ex 1781  df-sb 2070  df-clab 2800  df-cleq 2814  df-clel 2893  df-rab 3147  df-in 3943  df-res 5567

This theorem is referenced by:  reseq12i  5851  resindm  5900  resmpt  5905  resmpt3  5906  resmptf  5907  opabresid  5917  opabresidOLD  5919  rescnvcnv  6061  coires1  6117  fresaunres1  6551  fcoi1  6552  fninfp  6936  fvsnun1  6944  fvsnun2  6945  resoprab  7270  resmpo  7272  elrnmpores  7288  ofmres  7685  f1stres  7713  f2ndres  7714  df1st2  7793  df2nd2  7794  fsplitfpar  7814  dftpos2  7909  wfrlem14  7968  tfr2a  8031  tfr2b  8032  rdgseg  8058  frsucmpt2w  8075  frsucmpt2  8076  seqomlem2  8087  seqomlem3  8088  seqomlem4  8089  domss2  8676  dffi3  8895  fpwwe2lem13  10064  seqval  13381  hashgval  13694  hashinf  13696  submefmnd  18060  pgrpsubgsymg  18537  gsumzunsnd  19076  ablfac1b  19192  zzngim  20699  pmatcollpw3lem  21391  txflf  22614  xmsxmet2  23069  msmet2  23070  tmsxpsmopn  23147  isngp2  23206  subgnm  23242  tngngp2  23261  cnfldms  23384  msdcn  23449  oprpiece1res1  23555  oprpiece1res2  23556  isncvsngp  23753  cncms  23958  cnfldcusp  23960  reust  23984  minveclem3a  24030  dvreslem  24507  dvres2lem  24508  dvcmulf  24542  mdegfval  24656  psercn  25014  abelth  25029  efcvx  25037  efifo  25131  dfrelog  25149  dvrelog  25220  dvlog  25234  efopnlem2  25240  dvatan  25513  dchrisumlem1  26065  wlknwwlksnbij  27666  elimampt  30383  fnunres2  30424  df1stres  30439  df2ndres  30440  padct  30455  ressplusf  30637  ressnm  30638  gsummpt2d  30687  cycpmrn  30785  tocyccntz  30786  cycpmconjslem2  30797  qqhcn  31232  cnrrext  31251  rrhre  31262  esumcvg  31345  dya2icoseg2  31536  eulerpartgbij  31630  satf0  32619  trpred0  33075  frrlem12  33134  noetalem2  33218  noetalem3  33219  neibastop2  33709  mptsnunlem  34622  icorempo  34635  poimirlem3  34910  mbfposadd  34954  ftc1anclem3  34984  dvasin  34993  dvacos  34994  prdsbnd2  35088  repwsmet  35127  rrnequiv  35128  inres2  35521  xrnres  35665  xrnres2  35666  xrnres3  35667  diophin  39418  eldioph4b  39457  dnnumch1  39693  aomclem6  39708  radcnvrat  40695  lhe4.4ex1a  40710  dvsid  40712  dvsef  40713  imassmpt  41586  elicores  41858  climresmpt  41989  dvcosre  42245  dvmptresicc  42253  itgsinexplem1  42288  fourierdlem40  42481  fourierdlem57  42497  fourierdlem58  42498  fourierdlem62  42502  fourierdlem74  42514  fourierdlem75  42515  fourierdlem76  42516  fourierdlem80  42520  fourierdlem84  42524  fourierdlem85  42525  fourierdlem101  42541  fourierdlem102  42542  fourierdlem111  42551  fourierdlem114  42554  fouriersw  42565  fouriercn  42566  volicorescl  42884  fdmdifeqresdif  44439  aacllem  44951