Theorem reseq2i 6006

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

Syntax hints:   = wceq 1537   ↾ cres 5702

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1540  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-rab 3444  df-in 3983  df-opab 5229  df-xp 5706  df-res 5712

This theorem is referenced by:  reseq12i  6007  rescom  6032  resdmdfsn  6060  idinxpresid  6077  rescnvcnv  6235  resdm2  6262  funcnvres  6656  resasplit  6791  fresaunres2  6793  fresaunres1  6794  resdif  6883  resin  6884  funcocnv2  6887  fvn0ssdmfun  7108  residpr  7177  eqfunressuc  7397  fprlem1  8341  wfrlem5OLD  8369  domss2  9202  ordtypelem1  9587  frrlem15  9826  ackbij2lem3  10309  facnn  14324  fac0  14325  hashresfn  14389  relexpcnv  15084  divcnvshft  15903  ruclem4  16282  fsets  17216  setsid  17255  join0  18475  meet0  18476  symgfixelsi  19477  psgnsn  19562  dprd2da  20086  ply1plusgfvi  22264  uptx  23654  txcn  23655  ressxms  24559  ressms  24560  iscmet3lem3  25343  volres  25582  dvlip  26052  dvne0  26070  lhop  26075  dflog2  26620  dfrelog  26625  dvlog  26711  wilthlem2  27130  nosupbnd2lem1  27778  noinfbnd2lem1  27793  0grsubgr  29313  0pth  30157  1pthdlem1  30167  eupth2lemb  30269  ex-fpar  30494  fressupp  32700  df1stres  32715  df2ndres  32716  ffsrn  32743  resf1o  32744  fpwrelmapffs  32748  cycpmconjv  33135  sitmcl  34316  eulerpartlemn  34346  bnj1326  35002  satfv1lem  35330  divcnvlin  35695  poimirlem9  37589  zrdivrng  37913  isdrngo1  37916  ressucdifsn  38200  cnvresrn  38304  disjsuc  38715  eldioph4b  42767  diophren  42769  rclexi  43577  rtrclex  43579  cnvrcl0  43587  dfrtrcl5  43591  dfrcl2  43636  relexpiidm  43666  relexp01min  43675  relexpaddss  43680  seff  44278  sblpnf  44279  radcnvrat  44283  hashnzfzclim  44291  dvresioo  45842  fourierdlem72  46099  fourierdlem80  46107  fourierdlem94  46121  fourierdlem103  46130  fourierdlem104  46131  fourierdlem113  46140  fouriersw  46152  sge0split  46330  isubgrgrim  47781  rngcidALTV  47997  ringcidALTV  48031