Theorem reseq2i 5935

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

Syntax hints:   = wceq 1547   ↾ cres 5627

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2712

This theorem depends on definitions:  df-bi 208  df-an 397  df-tru 1550  df-ex 1787  df-sb 2074  df-clab 2719  df-cleq 2732  df-clel 2815  df-rab 3393  df-in 3897  df-opab 5142  df-xp 5631  df-res 5637

This theorem is referenced by:  reseq12i  5936  rescom  5961  resdmdfsn  5990  idinxpresid  6007  rescnvcnv  6162  resdm2  6189  funcnvres  6570  resasplit  6704  fresaunres2  6706  fresaunres1  6707  resdif  6795  resin  6796  funcocnv2  6799  fvn0ssdmfun  7022  residpr  7092  eqfunressuc  7312  fprlem1  8247  domss2  9071  ordtypelem1  9430  frrlem15  9679  ackbij2lem3  10160  facnn  14235  fac0  14236  hashresfn  14300  relexpcnv  14995  divcnvshft  15818  ruclem4  16199  fsets  17137  setsid  17175  join0  18367  meet0  18368  symgfixelsi  19408  psgnsn  19493  dprd2da  20017  ply1plusgfvi  22233  uptx  23615  txcn  23616  ressxms  24515  ressms  24516  iscmet3lem3  25282  volres  25520  dvlip  25985  dvne0  26003  lhop  26008  dflog2  26549  dfrelog  26554  dvlog  26640  wilthlem2  27057  nosupbnd2lem1  27704  noinfbnd2lem1  27719  0grsubgr  29372  0pth  30220  1pthdlem1  30230  eupth2lemb  30332  ex-fpar  30557  fressupp  32787  df1stres  32803  df2ndres  32804  ffsrn  32827  resf1o  32829  fpwrelmapffs  32833  cycpmconjv  33230  evlextv  33733  sitmcl  34542  eulerpartlemn  34572  bnj1326  35215  satfv1lem  35597  divcnvlin  35968  poimirlem9  38003  zrdivrng  38327  isdrngo1  38330  cnvresrn  38722  dfsucmap2  38838  ressucdifsn  38862  disjsuc  39233  eldioph4b  43263  diophren  43265  rclexi  44066  rtrclex  44068  cnvrcl0  44076  dfrtrcl5  44080  dfrcl2  44125  relexpiidm  44155  relexp01min  44164  relexpaddss  44169  seff  44760  sblpnf  44761  radcnvrat  44765  hashnzfzclim  44773  dvresioo  46371  fourierdlem72  46628  fourierdlem80  46636  fourierdlem94  46650  fourierdlem103  46659  fourierdlem104  46660  fourierdlem113  46669  fouriersw  46681  sge0split  46859  isubgrgrim  48427  stgr0  48458  stgr1  48459  rngcidALTV  48772  ringcidALTV  48806  tposresg  49375  tposres3  49378  tposresxp  49380