Theorem reseq2i 5966

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

This proof depends on syntax axioms:   = wceq 1569   ↾ cres 5652

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1572  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-rab 3413  df-in 4091  df-opab 5167  df-xp 5656  df-res 5662

This theorem is used by:  reseq12i  5967  rescom  5992  resindm  6018  resdmdfsn  6020  resdmdfsnOLD  6021  idinxpresid  6039  imadifssranOLD  6202  rescnvcnv  6205  resdm2  6232  funcnvres  6619  resasplit  6753  fresaunres2  6755  fresaunres1  6756  resdif  6847  resin  6848  funcocnv2  6851  fvn0ssdmfun  7075  residpr  7147  eqfunressuc  7372  fprlem1  8322  domss2  9159  ordtypelem1  9516  frrlem15  9765  ackbij2lem3  10322  facnn  14423  fac0  14424  hashresfn  14488  relexpcnv  15194  divcnvshft  16030  ruclem4  16408  fsets  17353  setsid  17391  join0  18583  meet0  18584  symgfixelsi  19655  psgnsn  19740  dprd2da  20264  ply1plusgfvi  22565  uptx  23950  txcn  23951  ressxms  24850  ressms  24851  iscmet3lem3  25617  volres  25855  dvlip  26319  dvne0  26337  lhop  26342  dflog2  26894  dfrelog  26899  dvlog  26985  wilthlem2  27402  nosupbnd2lem1  28078  noinfbnd2lem1  28093  0grsubgr  29865  0pth  30722  1pthdlem1  30732  eupth2lemb  30844  ex-fpar  31069  fressupp  33329  df1stres  33345  df2ndres  33346  ffsrn  33367  resf1o  33369  fpwrelmapffs  33373  cycpmconjv  33750  evlextv  34221  sitmcl  35030  eulerpartlemn  35060  bnj1326  35703  satfv1lem  36214  divcnvlin  36591  poimirlem9  38641  zrdivrng  38981  isdrngo1  38984  cnvresrn  39374  dfsucmap2  39490  ressucdifsn  39514  disjsuc  39885  eldioph4b  43912  diophren  43914  rclexi  44709  rtrclex  44711  cnvrcl0  44719  dfrtrcl5  44723  dfrcl2  44768  relexpiidm  44798  relexp01min  44807  relexpaddss  44812  seff  45387  sblpnf  45388  radcnvrat  45392  hashnzfzclim  45400  dvresioo  47025  fourierdlem72  47282  fourierdlem80  47290  fourierdlem94  47304  fourierdlem103  47313  fourierdlem104  47314  fourierdlem113  47323  fouriersw  47335  sge0split  47513  isubgrgrim  49121  stgr0  49152  stgr1  49153  rngcidALTV  49465  ringcidALTV  49499  tposresg  50085  tposres3  50088  tposresxp  50090  fucoisfunc  50581  fucoisfunc2lem1  50582