Theorem reseq2i 5981

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

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

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 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-rab 3417  df-in 4094  df-opab 5172  df-xp 5662  df-res 5668

This theorem is used by:  reseq12i  5982  rescom  6007  resindm  6035  resdmdfsn  6037  resdmdfsnOLD  6038  idinxpresid  6056  imadifssranOLD  6219  rescnvcnv  6222  resdm2  6249  idresrnsscocnv2  6280  funcnvres  6646  resasplit  6780  fresaunres2  6782  fresaunres1  6783  resdif  6874  resin  6875  funcocnv2  6878  funcocnv2OLD  6879  fvn0ssdmfun  7104  residpr  7176  eqfunressuc  7400  fprlem1  8354  domss2  9191  ordtypelem1  9547  frrlem15  9796  ackbij2lem3  10355  facnn  14458  fac0  14459  hashresfn  14523  relexpcnv  15229  divcnvshft  16065  ruclem4  16443  fsets  17388  setsid  17426  join0  18618  meet0  18619  symgfixelsi  19691  psgnsn  19776  dprd2da  20300  ply1plusgfvi  22603  uptx  23988  txcn  23989  ressxms  24888  ressms  24889  iscmet3lem3  25655  volres  25893  dvlip  26357  dvne0  26375  lhop  26380  dflog2  26934  dfrelog  26939  dvlog  27025  wilthlem2  27442  nosupbnd2lem1  28118  noinfbnd2lem1  28133  0grsubgr  29905  0pth  30762  1pthdlem1  30772  eupth2lemb  30884  ex-fpar  31109  fressupp  33368  df1stres  33384  df2ndres  33385  ffsrn  33406  resf1o  33408  fpwrelmapffs  33412  cycpmconjv  33792  fldedom  33950  evlextv  34278  sitmcl  35087  eulerpartlemn  35117  bnj1326  35760  satfv1lem  36328  divcnvlin  36706  bj-cnvresrn  38190  coss1b  38209  coss2b  38211  cossidres2  38214  cossididres  38217  coidmid  38218  nvo3  38223  poimirlem9  38808  zrdivrng  39146  isdrngo1  39149  cnvresrn  39539  dfsucmap2  39655  ressucdifsn  39679  disjsuc  40050  eldioph4b  44078  diophren  44080  rclexi  44870  rtrclex  44872  cnvrcl0  44880  dfrtrcl5  44884  dfrcl2  44929  relexpiidm  44959  relexp01min  44968  relexpaddss  44973  seff  45548  sblpnf  45549  radcnvrat  45553  hashnzfzclim  45561  dvresioo  47198  fourierdlem72  47455  fourierdlem80  47463  fourierdlem94  47477  fourierdlem103  47486  fourierdlem104  47487  fourierdlem113  47496  fouriersw  47508  sge0split  47686  isubgrgrim  49294  stgr0  49325  stgr1  49326  rngcidALTV  49638  ringcidALTV  49672  tposresg  50316  tposres3  50319  tposresxp  50321  fucoisfunc  50812  fucoisfunc2lem1  50813