Theorem reseq2i 5977

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

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

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 2148  ax-9 2156  ax-ext 2737

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2744  df-cleq 2757  df-clel 2840  df-rab 3419  df-in 3913  df-opab 5176  df-xp 5669  df-res 5675

This theorem is used by:  reseq12i  5978  rescom  6003  resindm  6031  resdmdfsn  6033  resdmdfsnOLD  6034  idinxpresid  6052  imadifssran  6204  rescnvcnv  6207  resdm2  6234  funcnvres  6618  resasplit  6752  fresaunres2  6754  fresaunres1  6755  resdif  6846  resin  6847  funcocnv2  6850  fvn0ssdmfun  7073  residpr  7143  eqfunressuc  7367  fprlem1  8299  domss2  9127  ordtypelem1  9483  frrlem15  9732  ackbij2lem3  10235  facnn  14324  fac0  14325  hashresfn  14389  relexpcnv  15091  divcnvshft  15927  ruclem4  16307  fsets  17246  setsid  17284  join0  18476  meet0  18477  symgfixelsi  19528  psgnsn  19613  dprd2da  20137  ply1plusgfvi  22430  uptx  23811  txcn  23812  ressxms  24711  ressms  24712  iscmet3lem3  25478  volres  25716  dvlip  26181  dvne0  26199  lhop  26204  dflog2  26754  dfrelog  26759  dvlog  26845  wilthlem2  27262  nosupbnd2lem1  27908  noinfbnd2lem1  27923  0grsubgr  29657  0pth  30505  1pthdlem1  30515  eupth2lemb  30617  ex-fpar  30842  fressupp  33062  df1stres  33078  df2ndres  33079  ffsrn  33102  resf1o  33104  fpwrelmapffs  33108  cycpmconjv  33485  evlextv  33955  sitmcl  34765  eulerpartlemn  34795  bnj1326  35438  satfv1lem  35867  divcnvlin  36238  poimirlem9  38313  zrdivrng  38637  isdrngo1  38640  cnvresrn  39030  dfsucmap2  39146  ressucdifsn  39170  disjsuc  39541  eldioph4b  43571  diophren  43573  rclexi  44374  rtrclex  44376  cnvrcl0  44384  dfrtrcl5  44388  dfrcl2  44433  relexpiidm  44463  relexp01min  44472  relexpaddss  44477  seff  45052  sblpnf  45053  radcnvrat  45057  hashnzfzclim  45065  dvresioo  46668  fourierdlem72  46925  fourierdlem80  46933  fourierdlem94  46947  fourierdlem103  46956  fourierdlem104  46957  fourierdlem113  46966  fouriersw  46978  sge0split  47156  isubgrgrim  48727  stgr0  48758  stgr1  48759  rngcidALTV  49072  ringcidALTV  49106  tposresg  49689  tposres3  49692  tposresxp  49694