Theorem reseq2i 5833

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

Syntax hints:   = wceq 1543   ↾ cres 5538

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2018  ax-8 2114  ax-9 2122  ax-ext 2708

This theorem depends on definitions:  df-bi 210  df-an 400  df-tru 1546  df-ex 1788  df-sb 2073  df-clab 2715  df-cleq 2728  df-clel 2809  df-rab 3060  df-in 3860  df-opab 5102  df-xp 5542  df-res 5548

This theorem is referenced by:  reseq12i  5834  rescom  5862  resdmdfsn  5886  idinxpresid  5900  rescnvcnv  6047  resdm2  6074  funcnvres  6436  resasplit  6567  fresaunres2  6569  fresaunres1  6570  resdif  6659  resin  6660  funcocnv2  6663  fvn0ssdmfun  6873  residpr  6936  fprlem1  8019  wfrlem5  8037  domss2  8783  ordtypelem1  9112  ackbij2lem3  9820  facnn  13806  fac0  13807  hashresfn  13871  relexpcnv  14563  divcnvshft  15382  ruclem4  15758  fsets  16698  setsid  16719  join0  17865  meet0  17866  symgfixelsi  18781  psgnsn  18866  dprd2da  19383  ply1plusgfvi  21117  uptx  22476  txcn  22477  ressxms  23377  ressms  23378  iscmet3lem3  24141  volres  24379  dvlip  24844  dvne0  24862  lhop  24867  dflog2  25403  dfrelog  25408  dvlog  25493  wilthlem2  25905  0grsubgr  27320  0pth  28162  1pthdlem1  28172  eupth2lemb  28274  ex-fpar  28499  fressupp  30696  df1stres  30710  df2ndres  30711  ffsrn  30738  resf1o  30739  fpwrelmapffs  30743  cycpmconjv  31082  sitmcl  31984  eulerpartlemn  32014  bnj1326  32673  satfv1lem  32991  divcnvlin  33367  eqfunressuc  33406  frrlem15  33505  nosupbnd2lem1  33604  noinfbnd2lem1  33619  poimirlem9  35472  zrdivrng  35797  isdrngo1  35800  cnvresrn  36169  eldioph4b  40277  diophren  40279  rclexi  40840  rtrclex  40842  cnvrcl0  40850  dfrtrcl5  40854  dfrcl2  40900  relexpiidm  40930  relexp01min  40939  relexpaddss  40944  seff  41541  sblpnf  41542  radcnvrat  41546  hashnzfzclim  41554  dvresioo  43080  fourierdlem72  43337  fourierdlem80  43345  fourierdlem94  43359  fourierdlem103  43368  fourierdlem104  43369  fourierdlem113  43378  fouriersw  43390  sge0split  43565  rngcidALTV  45165  ringcidALTV  45228