Theorem reseq1i 5255

Description: Equality inference for restrictions. (Contributed by NM, 21-Oct-2014.)

Hypothesis

Ref	Expression
reseqi.1	|- A = B

Assertion

Ref	Expression
reseq1i	|- ( A |` C ) = ( B |` C )

Proof of Theorem reseq1i

Step	Hyp	Ref	Expression
1		reseqi.1	. 2 |- A = B
2		reseq1 5253	. 2 |- ( A = B -> ( A |` C ) = ( B |` C ) )
3	1, 2	ax-mp 5	1 |- ( A |` C ) = ( B |` C )

Syntax hints:   = wceq 1381   |` cres 4987

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1603  ax-4 1616  ax-5 1689  ax-6 1732  ax-7 1774  ax-10 1821  ax-11 1826  ax-12 1838  ax-13 1983  ax-ext 2419

This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1384  df-ex 1598  df-nf 1602  df-sb 1725  df-clab 2427  df-cleq 2433  df-clel 2436  df-nfc 2591  df-v 3095  df-in 3465  df-res 4997

This theorem is referenced by:  reseq12i  5257  resindm  5304  resmpt  5309  resmpt3  5310  opabresid  5313  rescnvcnv  5456  coires1  5511  fresaunres1  5744  fcoi1  5745  fninfp  6079  fvsnun1  6087  fvsnun2  6088  resoprab  6379  resmpt2  6381  elrnmpt2res  6397  ofmres  6777  f1stres  6803  f2ndres  6804  df1st2  6867  df2nd2  6868  dftpos2  6970  tfr2a  7062  tfr2b  7063  rdgseg  7086  frsucmpt2  7103  seqomlem2  7114  seqomlem3  7115  seqomlem4  7116  domss2  7674  dffi3  7889  fpwwe2lem13  9018  seqval  12092  hashgval  12382  hashinf  12384  pgrpsubgsymg  16302  gsumzunsnd  16851  ablfac1b  16989  zzngim  18458  pmatcollpw3lem  19151  cnmptid  20028  txflf  20373  xmsxmet2  20828  msmet2  20829  tmsxpsmopn  20906  isngp2  20983  subgnm  21013  tngngp2  21032  cnfldms  21149  msdcn  21212  oprpiece1res1  21317  oprpiece1res2  21318  cncms  21661  cnfldcusp  21663  reust  21679  minveclem3a  21708  dvreslem  22179  dvres2lem  22180  dvcmulf  22214  mdegfval  22326  psercn  22686  abelth  22701  efcvx  22709  efifo  22799  dfrelog  22818  dvrelog  22883  dvlog  22897  efopnlem2  22903  dvatan  23131  dchrisumlem1  23539  constr3pthlem1  24520  resmptf  27362  df1stres  27387  df2ndres  27388  ressplusf  27504  ressnm  27505  qqhcn  27838  cnrrext  27857  rrhre  27865  esumcvg  27958  dya2icoseg2  28115  eulerpartgbij  28177  trpred0  29287  wfrlem14  29324  mbfposadd  30030  ftc1anclem3  30060  dvasin  30071  dvacos  30072  neibastop2  30147  prdsbnd2  30259  repwsmet  30298  rrnequiv  30299  diophin  30674  eldioph4b  30713  dnnumch1  30958  aomclem6  30973  radcnvrat  31164  lhe4.4ex1a  31203  dvsid  31205  dvsef  31206  dvcosre  31606  dvmptresicc  31616  itgsinexplem1  31638  fourierdlem40  31814  fourierdlem57  31831  fourierdlem58  31832  fourierdlem62  31836  fourierdlem74  31848  fourierdlem75  31849  fourierdlem76  31850  fourierdlem80  31854  fourierdlem84  31858  fourierdlem85  31859  fourierdlem101  31875  fourierdlem102  31876  fourierdlem111  31885  fourierdlem114  31888  fouriersw  31899  fouriercn  31900  fdmdifeqresdif  32639