Theorem reseq2i 5963

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

Syntax hints:   = wceq 1540   ↾ cres 5656

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 2007  ax-8 2110  ax-9 2118  ax-ext 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2065  df-clab 2714  df-cleq 2727  df-clel 2809  df-rab 3416  df-in 3933  df-opab 5182  df-xp 5660  df-res 5666

This theorem is referenced by:  reseq12i  5964  rescom  5989  resdmdfsn  6018  idinxpresid  6035  rescnvcnv  6193  resdm2  6220  funcnvres  6614  resasplit  6748  fresaunres2  6750  fresaunres1  6751  resdif  6839  resin  6840  funcocnv2  6843  fvn0ssdmfun  7064  residpr  7133  eqfunressuc  7354  fprlem1  8299  wfrlem5OLD  8327  domss2  9150  ordtypelem1  9532  frrlem15  9771  ackbij2lem3  10254  facnn  14293  fac0  14294  hashresfn  14358  relexpcnv  15054  divcnvshft  15871  ruclem4  16252  fsets  17188  setsid  17226  join0  18415  meet0  18416  symgfixelsi  19416  psgnsn  19501  dprd2da  20025  ply1plusgfvi  22177  uptx  23563  txcn  23564  ressxms  24464  ressms  24465  iscmet3lem3  25242  volres  25481  dvlip  25950  dvne0  25968  lhop  25973  dflog2  26521  dfrelog  26526  dvlog  26612  wilthlem2  27031  nosupbnd2lem1  27679  noinfbnd2lem1  27694  0grsubgr  29257  0pth  30106  1pthdlem1  30116  eupth2lemb  30218  ex-fpar  30443  fressupp  32665  df1stres  32681  df2ndres  32682  ffsrn  32706  resf1o  32707  fpwrelmapffs  32711  cycpmconjv  33153  sitmcl  34383  eulerpartlemn  34413  bnj1326  35057  satfv1lem  35384  divcnvlin  35750  poimirlem9  37653  zrdivrng  37977  isdrngo1  37980  ressucdifsn  38263  cnvresrn  38366  disjsuc  38777  eldioph4b  42834  diophren  42836  rclexi  43639  rtrclex  43641  cnvrcl0  43649  dfrtrcl5  43653  dfrcl2  43698  relexpiidm  43728  relexp01min  43737  relexpaddss  43742  seff  44333  sblpnf  44334  radcnvrat  44338  hashnzfzclim  44346  dvresioo  45950  fourierdlem72  46207  fourierdlem80  46215  fourierdlem94  46229  fourierdlem103  46238  fourierdlem104  46239  fourierdlem113  46248  fouriersw  46260  sge0split  46438  isubgrgrim  47942  stgr0  47972  stgr1  47973  rngcidALTV  48249  ringcidALTV  48283  tposresg  48853  tposres3  48856  tposresxp  48858