Theorem reseq2i 5900

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

Syntax hints:   = wceq 1539   ↾ cres 5602

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 1911  ax-6 1969  ax-7 2009  ax-8 2106  ax-9 2114  ax-ext 2707

This theorem depends on definitions:  df-bi 206  df-an 398  df-tru 1542  df-ex 1780  df-sb 2066  df-clab 2714  df-cleq 2728  df-clel 2814  df-rab 3306  df-in 3899  df-opab 5144  df-xp 5606  df-res 5612

This theorem is referenced by:  reseq12i  5901  rescom  5929  resdmdfsn  5953  idinxpresid  5967  rescnvcnv  6122  resdm2  6149  funcnvres  6541  resasplit  6674  fresaunres2  6676  fresaunres1  6677  resdif  6767  resin  6768  funcocnv2  6771  fvn0ssdmfun  6984  residpr  7047  fprlem1  8147  wfrlem5OLD  8175  domss2  8961  ordtypelem1  9325  frrlem15  9563  ackbij2lem3  10047  facnn  14039  fac0  14040  hashresfn  14104  relexpcnv  14795  divcnvshft  15616  ruclem4  15992  fsets  16919  setsid  16958  join0  18172  meet0  18173  symgfixelsi  19092  psgnsn  19177  dprd2da  19694  ply1plusgfvi  21462  uptx  22825  txcn  22826  ressxms  23730  ressms  23731  iscmet3lem3  24503  volres  24741  dvlip  25206  dvne0  25224  lhop  25229  dflog2  25765  dfrelog  25770  dvlog  25855  wilthlem2  26267  0grsubgr  27694  0pth  28538  1pthdlem1  28548  eupth2lemb  28650  ex-fpar  28875  fressupp  31071  df1stres  31085  df2ndres  31086  ffsrn  31113  resf1o  31114  fpwrelmapffs  31118  cycpmconjv  31458  sitmcl  32367  eulerpartlemn  32397  bnj1326  33055  satfv1lem  33373  divcnvlin  33747  eqfunressuc  33785  nosupbnd2lem1  33967  noinfbnd2lem1  33982  poimirlem9  35834  zrdivrng  36159  isdrngo1  36162  ressucdifsn  36452  cnvresrn  36561  disjsuc  36973  eldioph4b  40828  diophren  40830  rclexi  41436  rtrclex  41438  cnvrcl0  41446  dfrtrcl5  41450  dfrcl2  41495  relexpiidm  41525  relexp01min  41534  relexpaddss  41539  seff  42140  sblpnf  42141  radcnvrat  42145  hashnzfzclim  42153  dvresioo  43691  fourierdlem72  43948  fourierdlem80  43956  fourierdlem94  43970  fourierdlem103  43979  fourierdlem104  43980  fourierdlem113  43989  fouriersw  44001  sge0split  44177  rngcidALTV  45793  ringcidALTV  45856