Theorem reseq2i 5977

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

Syntax hints:   = wceq 1539   ↾ cres 5677

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 2701

This theorem depends on definitions:  df-bi 206  df-an 395  df-tru 1542  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2722  df-clel 2808  df-rab 3431  df-in 3954  df-opab 5210  df-xp 5681  df-res 5687

This theorem is referenced by:  reseq12i  5978  rescom  6006  resdmdfsn  6030  idinxpresid  6046  rescnvcnv  6202  resdm2  6229  funcnvres  6625  resasplit  6760  fresaunres2  6762  fresaunres1  6763  resdif  6853  resin  6854  funcocnv2  6857  fvn0ssdmfun  7075  residpr  7142  eqfunressuc  7360  fprlem1  8287  wfrlem5OLD  8315  domss2  9138  ordtypelem1  9515  frrlem15  9754  ackbij2lem3  10238  facnn  14239  fac0  14240  hashresfn  14304  relexpcnv  14986  divcnvshft  15805  ruclem4  16181  fsets  17106  setsid  17145  join0  18362  meet0  18363  symgfixelsi  19344  psgnsn  19429  dprd2da  19953  ply1plusgfvi  21984  uptx  23349  txcn  23350  ressxms  24254  ressms  24255  iscmet3lem3  25038  volres  25277  dvlip  25745  dvne0  25763  lhop  25768  dflog2  26305  dfrelog  26310  dvlog  26395  wilthlem2  26809  nosupbnd2lem1  27454  noinfbnd2lem1  27469  0grsubgr  28802  0pth  29645  1pthdlem1  29655  eupth2lemb  29757  ex-fpar  29982  fressupp  32177  df1stres  32192  df2ndres  32193  ffsrn  32221  resf1o  32222  fpwrelmapffs  32226  cycpmconjv  32571  sitmcl  33648  eulerpartlemn  33678  bnj1326  34335  satfv1lem  34651  divcnvlin  35006  poimirlem9  36800  zrdivrng  37124  isdrngo1  37127  ressucdifsn  37414  cnvresrn  37520  disjsuc  37932  eldioph4b  41851  diophren  41853  rclexi  42668  rtrclex  42670  cnvrcl0  42678  dfrtrcl5  42682  dfrcl2  42727  relexpiidm  42757  relexp01min  42766  relexpaddss  42771  seff  43370  sblpnf  43371  radcnvrat  43375  hashnzfzclim  43383  dvresioo  44935  fourierdlem72  45192  fourierdlem80  45200  fourierdlem94  45214  fourierdlem103  45223  fourierdlem104  45224  fourierdlem113  45233  fouriersw  45245  sge0split  45423  rngcidALTV  46977  ringcidALTV  47040