Theorem reseq2i 5314

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

Syntax hints:   = wceq 1475   ↾ cres 5040

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-v 3175  df-in 3547  df-opab 4644  df-xp 5044  df-res 5050

This theorem is referenced by:  reseq12i  5315  rescom  5343  resdmdfsn  5365  rescnvcnv  5515  resdm2  5542  funcnvres  5881  resasplit  5987  fresaunres2  5989  fresaunres1  5990  resdif  6070  resin  6071  funcocnv2  6074  fvn0ssdmfun  6258  residpr  6315  wfrlem5  7306  domss2  8004  ordtypelem1  8306  ackbij2lem3  8946  facnn  12924  fac0  12925  hashresfn  12990  relexpcnv  13623  divcnvshft  14426  ruclem4  14802  fsets  15723  setsid  15742  meet0  16960  join0  16961  symgfixelsi  17678  psgnsn  17763  dprd2da  18264  ply1plusgfvi  19433  uptx  21238  txcn  21239  ressxms  22140  ressms  22141  iscmet3lem3  22896  volres  23103  dvlip  23560  dvne0  23578  lhop  23583  dflog2  24111  dfrelog  24116  dvlog  24197  wilthlem2  24595  0pth  26100  2pthlem1  26125  df1stres  28864  df2ndres  28865  ffsrn  28892  resf1o  28893  fpwrelmapffs  28897  sitmcl  29740  eulerpartlemn  29770  bnj1326  30348  divcnvlin  30871  frrlem5  31028  poimirlem9  32588  zrdivrng  32922  isdrngo1  32925  eldioph4b  36393  diophren  36395  rclexi  36941  rtrclex  36943  cnvrcl0  36951  dfrtrcl5  36955  dfrcl2  36985  relexpiidm  37015  relexp01min  37024  relexpaddss  37029  seff  37530  sblpnf  37531  radcnvrat  37535  hashnzfzclim  37543  dvresioo  38811  fourierdlem72  39071  fourierdlem80  39079  fourierdlem94  39093  fourierdlem103  39102  fourierdlem104  39103  fourierdlem113  39112  fouriersw  39124  sge0split  39302  0grsubgr  40502  0pth-av  41293  1pthdlem1  41302  eupth2lemb  41405  rngcidALTV  41783  ringcidALTV  41846