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 1541   ↾ cres 5626

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2715  df-cleq 2728  df-clel 2811  df-rab 3400  df-in 3908  df-opab 5161  df-xp 5630  df-res 5636

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  7019  residpr  7088  eqfunressuc  7307  fprlem1  8242  domss2  9064  ordtypelem1  9423  frrlem15  9669  ackbij2lem3  10150  facnn  14198  fac0  14199  hashresfn  14263  relexpcnv  14958  divcnvshft  15778  ruclem4  16159  fsets  17096  setsid  17134  join0  18326  meet0  18327  symgfixelsi  19364  psgnsn  19449  dprd2da  19973  ply1plusgfvi  22182  uptx  23569  txcn  23570  ressxms  24469  ressms  24470  iscmet3lem3  25246  volres  25485  dvlip  25954  dvne0  25972  lhop  25977  dflog2  26525  dfrelog  26530  dvlog  26616  wilthlem2  27035  nosupbnd2lem1  27683  noinfbnd2lem1  27698  0grsubgr  29351  0pth  30200  1pthdlem1  30210  eupth2lemb  30312  ex-fpar  30537  fressupp  32767  df1stres  32783  df2ndres  32784  ffsrn  32807  resf1o  32809  fpwrelmapffs  32813  cycpmconjv  33224  evlextv  33707  sitmcl  34508  eulerpartlemn  34538  bnj1326  35182  satfv1lem  35556  divcnvlin  35927  poimirlem9  37826  zrdivrng  38150  isdrngo1  38153  cnvresrn  38537  dfsucmap2  38634  ressucdifsn  38657  disjsuc  39014  eldioph4b  43049  diophren  43051  rclexi  43852  rtrclex  43854  cnvrcl0  43862  dfrtrcl5  43866  dfrcl2  43911  relexpiidm  43941  relexp01min  43950  relexpaddss  43955  seff  44546  sblpnf  44547  radcnvrat  44551  hashnzfzclim  44559  dvresioo  46161  fourierdlem72  46418  fourierdlem80  46426  fourierdlem94  46440  fourierdlem103  46449  fourierdlem104  46450  fourierdlem113  46459  fouriersw  46471  sge0split  46649  isubgrgrim  48171  stgr0  48202  stgr1  48203  rngcidALTV  48516  ringcidALTV  48550  tposresg  49119  tposres3  49122  tposresxp  49124