Theorem reseq2i 5885

Description: Equality inference for restrictions. (Contributed by Paul Chapman, 22-Jun-2011.)

Hypothesis

Ref	Expression
reseqi.1	⊢ 𝐴 = 𝐵

Assertion

Ref	Expression
reseq2i	⊢ (𝐶 ↾ 𝐴) = (𝐶 ↾ 𝐵)

Proof of Theorem reseq2i

Step	Hyp	Ref	Expression
1		reseqi.1	. 2 ⊢ 𝐴 = 𝐵
2		reseq2 5883	. 2 ⊢ (𝐴 = 𝐵 → (𝐶 ↾ 𝐴) = (𝐶 ↾ 𝐵))
3	1, 2	ax-mp 5	1 ⊢ (𝐶 ↾ 𝐴) = (𝐶 ↾ 𝐵)

Syntax hints:   = wceq 1541   ↾ cres 5590

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1801  ax-4 1815  ax-5 1916  ax-6 1974  ax-7 2014  ax-8 2111  ax-9 2119  ax-ext 2710

This theorem depends on definitions:  df-bi 206  df-an 396  df-tru 1544  df-ex 1786  df-sb 2071  df-clab 2717  df-cleq 2731  df-clel 2817  df-rab 3074  df-in 3898  df-opab 5141  df-xp 5594  df-res 5600

This theorem is referenced by:  reseq12i  5886  rescom  5914  resdmdfsn  5938  idinxpresid  5952  rescnvcnv  6104  resdm2  6131  funcnvres  6508  resasplit  6640  fresaunres2  6642  fresaunres1  6643  resdif  6732  resin  6733  funcocnv2  6736  fvn0ssdmfun  6946  residpr  7009  fprlem1  8100  wfrlem5OLD  8128  domss2  8888  ordtypelem1  9238  frrlem15  9499  ackbij2lem3  9981  facnn  13970  fac0  13971  hashresfn  14035  relexpcnv  14727  divcnvshft  15548  ruclem4  15924  fsets  16851  setsid  16890  join0  18104  meet0  18105  symgfixelsi  19024  psgnsn  19109  dprd2da  19626  ply1plusgfvi  21394  uptx  22757  txcn  22758  ressxms  23662  ressms  23663  iscmet3lem3  24435  volres  24673  dvlip  25138  dvne0  25156  lhop  25161  dflog2  25697  dfrelog  25702  dvlog  25787  wilthlem2  26199  0grsubgr  27626  0pth  28468  1pthdlem1  28478  eupth2lemb  28580  ex-fpar  28805  fressupp  31001  df1stres  31015  df2ndres  31016  ffsrn  31043  resf1o  31044  fpwrelmapffs  31048  cycpmconjv  31388  sitmcl  32297  eulerpartlemn  32327  bnj1326  32985  satfv1lem  33303  divcnvlin  33677  eqfunressuc  33715  nosupbnd2lem1  33897  noinfbnd2lem1  33912  poimirlem9  35765  zrdivrng  36090  isdrngo1  36093  cnvresrn  36462  eldioph4b  40613  diophren  40615  rclexi  41176  rtrclex  41178  cnvrcl0  41186  dfrtrcl5  41190  dfrcl2  41235  relexpiidm  41265  relexp01min  41274  relexpaddss  41279  seff  41880  sblpnf  41881  radcnvrat  41885  hashnzfzclim  41893  dvresioo  43416  fourierdlem72  43673  fourierdlem80  43681  fourierdlem94  43695  fourierdlem103  43704  fourierdlem104  43705  fourierdlem113  43714  fouriersw  43726  sge0split  43901  rngcidALTV  45501  ringcidALTV  45564