Theorem reseq2i 5969

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

This proof depends on syntax axioms:   = wceq 1570   ↾ cres 5657

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2739  df-cleq 2752  df-clel 2835  df-rab 3413  df-in 3906  df-opab 5168  df-xp 5661  df-res 5667

This theorem is used by:  reseq12i  5970  rescom  5995  resindm  6023  resdmdfsn  6025  resdmdfsnOLD  6026  idinxpresid  6044  imadifssran  6197  rescnvcnv  6200  resdm2  6227  funcnvres  6611  resasplit  6745  fresaunres2  6747  fresaunres1  6748  resdif  6839  resin  6840  funcocnv2  6843  fvn0ssdmfun  7067  residpr  7139  eqfunressuc  7364  fprlem1  8299  domss2  9134  ordtypelem1  9490  frrlem15  9739  ackbij2lem3  10242  facnn  14339  fac0  14340  hashresfn  14404  relexpcnv  15108  divcnvshft  15944  ruclem4  16322  fsets  17261  setsid  17299  join0  18491  meet0  18492  symgfixelsi  19562  psgnsn  19647  dprd2da  20171  ply1plusgfvi  22466  uptx  23851  txcn  23852  ressxms  24751  ressms  24752  iscmet3lem3  25518  volres  25756  dvlip  26220  dvne0  26238  lhop  26243  dflog2  26797  dfrelog  26802  dvlog  26888  wilthlem2  27305  nosupbnd2lem1  27951  noinfbnd2lem1  27966  0grsubgr  29738  0pth  30595  1pthdlem1  30605  eupth2lemb  30717  ex-fpar  30942  fressupp  33160  df1stres  33176  df2ndres  33177  ffsrn  33199  resf1o  33201  fpwrelmapffs  33205  cycpmconjv  33582  evlextv  34052  sitmcl  34862  eulerpartlemn  34892  bnj1326  35535  satfv1lem  35941  divcnvlin  36312  poimirlem9  38378  zrdivrng  38703  isdrngo1  38706  cnvresrn  39096  dfsucmap2  39212  ressucdifsn  39236  disjsuc  39607  eldioph4b  43652  diophren  43654  rclexi  44455  rtrclex  44457  cnvrcl0  44465  dfrtrcl5  44469  dfrcl2  44514  relexpiidm  44544  relexp01min  44553  relexpaddss  44558  seff  45133  sblpnf  45134  radcnvrat  45138  hashnzfzclim  45146  dvresioo  46749  fourierdlem72  47006  fourierdlem80  47014  fourierdlem94  47028  fourierdlem103  47037  fourierdlem104  47038  fourierdlem113  47047  fouriersw  47059  sge0split  47237  isubgrgrim  48845  stgr0  48876  stgr1  48877  rngcidALTV  49189  ringcidALTV  49223  tposresg  49804  tposres3  49807  tposresxp  49809