Theorem reseq2i 5939

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

Syntax hints:   = wceq 1541   ↾ cres 5640

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2702

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1544  df-ex 1782  df-sb 2068  df-clab 2709  df-cleq 2723  df-clel 2809  df-rab 3406  df-in 3920  df-opab 5173  df-xp 5644  df-res 5650

This theorem is referenced by:  reseq12i  5940  rescom  5968  resdmdfsn  5992  idinxpresid  6006  rescnvcnv  6161  resdm2  6188  funcnvres  6584  resasplit  6717  fresaunres2  6719  fresaunres1  6720  resdif  6810  resin  6811  funcocnv2  6814  fvn0ssdmfun  7030  residpr  7094  eqfunressuc  7311  fprlem1  8236  wfrlem5OLD  8264  domss2  9087  ordtypelem1  9463  frrlem15  9702  ackbij2lem3  10186  facnn  14185  fac0  14186  hashresfn  14250  relexpcnv  14932  divcnvshft  15751  ruclem4  16127  fsets  17052  setsid  17091  join0  18308  meet0  18309  symgfixelsi  19231  psgnsn  19316  dprd2da  19835  ply1plusgfvi  21650  uptx  23013  txcn  23014  ressxms  23918  ressms  23919  iscmet3lem3  24691  volres  24929  dvlip  25394  dvne0  25412  lhop  25417  dflog2  25953  dfrelog  25958  dvlog  26043  wilthlem2  26455  nosupbnd2lem1  27100  noinfbnd2lem1  27115  0grsubgr  28289  0pth  29132  1pthdlem1  29142  eupth2lemb  29244  ex-fpar  29469  fressupp  31670  df1stres  31685  df2ndres  31686  ffsrn  31714  resf1o  31715  fpwrelmapffs  31719  cycpmconjv  32061  sitmcl  33040  eulerpartlemn  33070  bnj1326  33727  satfv1lem  34043  divcnvlin  34391  poimirlem9  36160  zrdivrng  36485  isdrngo1  36488  ressucdifsn  36775  cnvresrn  36882  disjsuc  37294  eldioph4b  41192  diophren  41194  rclexi  42009  rtrclex  42011  cnvrcl0  42019  dfrtrcl5  42023  dfrcl2  42068  relexpiidm  42098  relexp01min  42107  relexpaddss  42112  seff  42711  sblpnf  42712  radcnvrat  42716  hashnzfzclim  42724  dvresioo  44282  fourierdlem72  44539  fourierdlem80  44547  fourierdlem94  44561  fourierdlem103  44570  fourierdlem104  44571  fourierdlem113  44580  fouriersw  44592  sge0split  44770  rngcidALTV  46409  ringcidALTV  46472