Theorem reseq2i 5936

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

Syntax hints:   = wceq 1540   ↾ cres 5633

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-rab 3403  df-in 3918  df-opab 5165  df-xp 5637  df-res 5643

This theorem is referenced by:  reseq12i  5937  rescom  5962  resdmdfsn  5991  idinxpresid  6008  rescnvcnv  6165  resdm2  6192  funcnvres  6578  resasplit  6712  fresaunres2  6714  fresaunres1  6715  resdif  6803  resin  6804  funcocnv2  6807  fvn0ssdmfun  7028  residpr  7097  eqfunressuc  7318  fprlem1  8256  domss2  9077  ordtypelem1  9447  frrlem15  9686  ackbij2lem3  10169  facnn  14216  fac0  14217  hashresfn  14281  relexpcnv  14977  divcnvshft  15797  ruclem4  16178  fsets  17115  setsid  17153  join0  18340  meet0  18341  symgfixelsi  19341  psgnsn  19426  dprd2da  19950  ply1plusgfvi  22102  uptx  23488  txcn  23489  ressxms  24389  ressms  24390  iscmet3lem3  25166  volres  25405  dvlip  25874  dvne0  25892  lhop  25897  dflog2  26445  dfrelog  26450  dvlog  26536  wilthlem2  26955  nosupbnd2lem1  27603  noinfbnd2lem1  27618  0grsubgr  29181  0pth  30027  1pthdlem1  30037  eupth2lemb  30139  ex-fpar  30364  fressupp  32584  df1stres  32600  df2ndres  32601  ffsrn  32625  resf1o  32626  fpwrelmapffs  32630  cycpmconjv  33072  sitmcl  34315  eulerpartlemn  34345  bnj1326  34989  satfv1lem  35322  divcnvlin  35693  poimirlem9  37596  zrdivrng  37920  isdrngo1  37923  ressucdifsn  38206  cnvresrn  38303  disjsuc  38724  eldioph4b  42772  diophren  42774  rclexi  43577  rtrclex  43579  cnvrcl0  43587  dfrtrcl5  43591  dfrcl2  43636  relexpiidm  43666  relexp01min  43675  relexpaddss  43680  seff  44271  sblpnf  44272  radcnvrat  44276  hashnzfzclim  44284  dvresioo  45892  fourierdlem72  46149  fourierdlem80  46157  fourierdlem94  46171  fourierdlem103  46180  fourierdlem104  46181  fourierdlem113  46190  fouriersw  46202  sge0split  46380  isubgrgrim  47902  stgr0  47932  stgr1  47933  rngcidALTV  48235  ringcidALTV  48269  tposresg  48839  tposres3  48842  tposresxp  48844