Theorem reseq1i 5204

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 5202	. 2 |- ( A = B -> ( A |` C ) = ( B |` C ) )
3	1, 2	ax-mp 5	1 |- ( A |` C ) = ( B |` C )

Syntax hints:   = wceq 1370   |` cres 4940

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-10 1777  ax-11 1782  ax-12 1794  ax-13 1952  ax-ext 2430

This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1703  df-clab 2437  df-cleq 2443  df-clel 2446  df-nfc 2601  df-v 3070  df-in 3433  df-res 4950

This theorem is referenced by:  reseq12i  5206  resindm  5249  resmpt  5254  resmpt3  5255  opabresid  5257  rescnvcnv  5399  coires1  5453  fresaunres1  5682  fcoi1  5683  fninfp  6004  fvsnun1  6012  fvsnun2  6013  resoprab  6286  resmpt2  6288  elrnmpt2res  6304  ofmres  6673  f1stres  6698  f2ndres  6699  df1st2  6759  df2nd2  6760  dftpos2  6862  tfr2a  6954  tfr2b  6955  rdgseg  6978  frsucmpt2  6995  seqomlem2  7006  seqomlem3  7007  seqomlem4  7008  domss2  7570  dffi3  7782  fpwwe2lem13  8910  seqval  11918  hashgval  12207  hashinf  12209  pgrpsubgsymg  16015  gsumzunsnd  16556  ablfac1b  16676  zzngim  18094  cnmptid  19350  txflf  19695  xmsxmet2  20150  msmet2  20151  tmsxpsmopn  20228  isngp2  20305  subgnm  20335  tngngp2  20354  cnfldms  20471  msdcn  20534  oprpiece1res1  20639  oprpiece1res2  20640  cncms  20983  cnfldcusp  20985  reust  21001  minveclem3a  21030  dvreslem  21500  dvres2lem  21501  dvcmulf  21535  mdegfval  21647  psercn  22007  abelth  22022  efcvx  22030  efifo  22119  dfrelog  22133  dvrelog  22198  dvlog  22212  efopnlem2  22218  dvatan  22446  dchrisumlem1  22854  constr3pthlem1  23676  resmptf  26108  df1stres  26133  df2ndres  26134  ressplusf  26245  ressnm  26246  qqhcn  26554  cnrrext  26573  rrhre  26581  esumcvg  26669  dya2icoseg2  26827  eulerpartgbij  26889  trpred0  27834  wfrlem14  27871  mbfposadd  28577  ftc1anclem3  28607  dvasin  28618  dvacos  28619  neibastop2  28720  prdsbnd2  28832  repwsmet  28871  rrnequiv  28872  diophin  29249  eldioph4b  29288  dnnumch1  29535  aomclem6  29550  lhe4.4ex1a  29741  dvsid  29743  dvsef  29744  dvcosre  29926  itgsinexplem1  29932  fdmdifeqresdif  30870  pmatcollpw4fi  31241