Theorem reseq1i 5934

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

Syntax hints:   = wceq 1542   ↾ cres 5626

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-rab 3391  df-in 3897  df-res 5636

This theorem is referenced by:  reseq12i  5936  resindm  5989  resmpt  5996  resmpt3  5997  resmptf  5998  elimampt  6002  opabresid  6009  rescnvcnv  6162  coires1  6223  fnunres2  6605  fresaunres1  6707  fcoi1  6708  fninfp  7122  fvsnun1  7130  fvsnun2  7131  resoprab  7478  resmpo  7480  elimampo  7497  elrnmpores  7498  ofmres  7930  f1stres  7959  f2ndres  7960  df1st2  8041  df2nd2  8042  fsplitfpar  8061  dftpos2  8186  frrlem12  8240  tfr2a  8327  tfr2b  8328  rdgseg  8354  frsucmpt2  8372  seqomlem2  8383  seqomlem3  8384  seqomlem4  8385  domss2  9067  dffi3  9337  axdc  10434  fpwwe2lem12  10556  seqval  13965  hashgval  14286  hashinf  14288  submefmnd  18854  pgrpsubgsymg  19375  gsumzunsnd  19922  ablfac1b  20038  zzngim  21542  pmatcollpw3lem  22758  txflf  23981  xmsxmet2  24434  msmet2  24435  tmsxpsmopn  24512  isngp2  24572  subgnm  24608  tngngp2  24627  cnfldms  24750  msdcn  24817  oprpiece1res1  24928  oprpiece1res2  24929  isncvsngp  25126  cncms  25332  cnfldcusp  25334  reust  25358  minveclem3a  25404  dvreslem  25886  dvres2lem  25887  dvmptresicc  25893  dvcmulf  25922  mdegfval  26037  psercn  26404  abelth  26419  efcvx  26427  efifo  26524  dfrelog  26542  dvrelog  26614  dvlog  26628  efopnlem2  26634  dvatan  26912  dchrisumlem1  27466  noetasuplem2  27712  noetasuplem3  27713  noetasuplem4  27714  noetainflem2  27716  wlknwwlksnbij  29971  df1stres  32792  df2ndres  32793  padct  32806  ressplusf  33038  ressnm  33039  gsummpt2d  33125  cycpmrn  33219  tocyccntz  33220  cycpmconjslem2  33231  qusima  33483  qqhcn  34151  cnrrext  34170  rrhre  34181  esumcvg  34246  dya2icoseg2  34438  eulerpartgbij  34532  satf0  35570  neibastop2  36559  mptsnunlem  37668  icorempo  37681  poimirlem3  37958  mbfposadd  38002  ftc1anclem3  38030  dvasin  38039  dvacos  38040  prdsbnd2  38130  repwsmet  38169  rrnequiv  38170  inres2  38582  xrnres  38760  xrnres2  38761  xrnres3  38762  diophin  43218  eldioph4b  43257  dnnumch1  43490  aomclem6  43505  radcnvrat  44759  lhe4.4ex1a  44774  dvsid  44776  dvsef  44777  imassmpt  45709  elicores  45981  climresmpt  46105  dvcosre  46358  itgsinexplem1  46400  fourierdlem40  46593  fourierdlem57  46609  fourierdlem58  46610  fourierdlem62  46614  fourierdlem74  46626  fourierdlem75  46627  fourierdlem76  46628  fourierdlem80  46632  fourierdlem84  46636  fourierdlem85  46637  fourierdlem101  46653  fourierdlem102  46654  fourierdlem111  46663  fourierdlem114  46666  fouriersw  46677  fouriercn  46678  volicorescl  46999  fdmdifeqresdif  48830  tposresg  49365  tposrescnv  49366  rescofuf  49580  aacllem  50288