Theorem reseq1i 5966

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

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

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 2147  ax-9 2155  ax-ext 2733

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-sb 2100  df-clab 2740  df-cleq 2753  df-clel 2836  df-rab 3414  df-in 3906  df-res 5663

This theorem is used by:  reseq12i  5968  resindmOLD  6022  resmpt  6031  resmpt3  6032  resmptf  6033  elimampt  6037  opabresid  6044  rescnvcnv  6198  coires1  6259  fnunres2  6644  fresaunres1  6747  fcoi1  6748  fninfp  7171  fvsnun1  7179  fvsnun2  7180  resoprab  7530  resmpo  7532  elimampo  7549  elrnmpores  7550  ofmres  7985  f1stres  8014  f2ndres  8015  df1st2  8098  df2nd2  8099  fsplitfpar  8118  dftpos2  8244  frrlem12  8299  tfr2a  8387  tfr2b  8388  rdgseg  8414  frsucmpt2  8432  seqomlem2  8445  seqomlem3  8446  seqomlem4  8447  domss2  9139  dffi3  9407  axdc  10580  fpwwe2lem12  10708  seqval  14135  hashgval  14457  hashinf  14459  submefmnd  19071  pgrpsubgsymg  19603  gsumzunsnd  20150  ablfac1b  20266  zzngim  21838  pmatcollpw3lem  23081  txflf  24305  xmsxmet2  24758  msmet2  24759  tmsxpsmopn  24836  isngp2  24896  subgnm  24932  tngngp2  24951  cnfldms  25074  msdcn  25141  oprpiece1res1  25252  oprpiece1res2  25253  isncvsngp  25450  cncms  25656  cnfldcusp  25658  reust  25682  minveclem3a  25728  dvreslem  26209  dvres2lem  26210  dvmptresicc  26216  dvcmulf  26245  mdegfval  26360  psercn  26735  abelth  26750  efcvx  26758  efifo  26857  dfrelog  26875  dvrelog  26947  dvlog  26961  efopnlem2  26967  dvatan  27245  dchrisumlem1  27798  noetasuplem2  28073  noetasuplem3  28074  noetasuplem4  28075  noetainflem2  28077  wlknwwlksnbij  30459  df1stres  33279  df2ndres  33280  padct  33292  ressplusf  33506  ressnm  33507  gsummpt2d  33592  cycpmrn  33686  tocyccntz  33687  cycpmconjslem2  33698  qusima  33941  qqhcn  34605  cnrrext  34624  rrhre  34635  esumcvg  34700  dya2icoseg2  34893  eulerpartgbij  34987  satf0  36106  neibastop2  37119  mptsnunlem  38229  icorempo  38242  poimirlem3  38509  mbfposadd  38553  ftc1anclem3  38581  dvasin  38590  dvacos  38591  prdsbnd2  38697  repwsmet  38736  rrnequiv  38737  inres2  39147  xrnres  39325  xrnres2  39326  xrnres3  39327  diophin  43736  eldioph4b  43771  dnnumch1  44004  aomclem6  44019  radcnvrat  45257  lhe4.4ex1a  45272  dvsid  45274  dvsef  45275  imassmpt  46217  elicores  46489  climresmpt  46613  dvcosre  46866  itgsinexplem1  46908  fourierdlem40  47101  fourierdlem57  47117  fourierdlem58  47118  fourierdlem62  47122  fourierdlem74  47134  fourierdlem75  47135  fourierdlem76  47136  fourierdlem80  47140  fourierdlem84  47144  fourierdlem85  47145  fourierdlem101  47161  fourierdlem102  47162  fourierdlem111  47171  fourierdlem114  47174  fouriersw  47185  fouriercn  47186  volicorescl  47507  fdmdifeqresdif  49398  tposresg  49930  tposrescnv  49931  rescofuf  50145  aacllem  50883