Theorem reseq2i 5976

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

Syntax hints:   = wceq 1542   ↾ cres 5677

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-rab 3434  df-in 3954  df-opab 5210  df-xp 5681  df-res 5687

This theorem is referenced by:  reseq12i  5977  rescom  6005  resdmdfsn  6029  idinxpresid  6045  rescnvcnv  6200  resdm2  6227  funcnvres  6623  resasplit  6758  fresaunres2  6760  fresaunres1  6761  resdif  6851  resin  6852  funcocnv2  6855  fvn0ssdmfun  7072  residpr  7136  eqfunressuc  7353  fprlem1  8280  wfrlem5OLD  8308  domss2  9132  ordtypelem1  9509  frrlem15  9748  ackbij2lem3  10232  facnn  14231  fac0  14232  hashresfn  14296  relexpcnv  14978  divcnvshft  15797  ruclem4  16173  fsets  17098  setsid  17137  join0  18354  meet0  18355  symgfixelsi  19296  psgnsn  19381  dprd2da  19904  ply1plusgfvi  21746  uptx  23111  txcn  23112  ressxms  24016  ressms  24017  iscmet3lem3  24789  volres  25027  dvlip  25492  dvne0  25510  lhop  25515  dflog2  26051  dfrelog  26056  dvlog  26141  wilthlem2  26553  nosupbnd2lem1  27198  noinfbnd2lem1  27213  0grsubgr  28515  0pth  29358  1pthdlem1  29368  eupth2lemb  29470  ex-fpar  29695  fressupp  31888  df1stres  31903  df2ndres  31904  ffsrn  31932  resf1o  31933  fpwrelmapffs  31937  cycpmconjv  32279  sitmcl  33288  eulerpartlemn  33318  bnj1326  33975  satfv1lem  34291  divcnvlin  34640  poimirlem9  36435  zrdivrng  36759  isdrngo1  36762  ressucdifsn  37049  cnvresrn  37155  disjsuc  37567  eldioph4b  41482  diophren  41484  rclexi  42299  rtrclex  42301  cnvrcl0  42309  dfrtrcl5  42313  dfrcl2  42358  relexpiidm  42388  relexp01min  42397  relexpaddss  42402  seff  43001  sblpnf  43002  radcnvrat  43006  hashnzfzclim  43014  dvresioo  44572  fourierdlem72  44829  fourierdlem80  44837  fourierdlem94  44851  fourierdlem103  44860  fourierdlem104  44861  fourierdlem113  44870  fouriersw  44882  sge0split  45060  rngcidALTV  46791  ringcidALTV  46854