Theorem reseq2i 5967

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

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

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 2733

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2740  df-cleq 2753  df-clel 2836  df-rab 3414  df-in 3906  df-opab 5168  df-xp 5657  df-res 5663

This theorem is used by:  reseq12i  5968  rescom  5993  resindm  6019  resdmdfsn  6021  resdmdfsnOLD  6022  idinxpresid  6040  imadifssranOLD  6201  rescnvcnv  6204  resdm2  6231  funcnvres  6616  resasplit  6750  fresaunres2  6752  fresaunres1  6753  resdif  6844  resin  6845  funcocnv2  6848  fvn0ssdmfun  7072  residpr  7144  eqfunressuc  7369  fprlem1  8311  domss2  9148  ordtypelem1  9505  frrlem15  9754  ackbij2lem3  10311  facnn  14412  fac0  14413  hashresfn  14477  relexpcnv  15181  divcnvshft  16017  ruclem4  16395  fsets  17340  setsid  17378  join0  18570  meet0  18571  symgfixelsi  19642  psgnsn  19727  dprd2da  20251  ply1plusgfvi  22552  uptx  23937  txcn  23938  ressxms  24837  ressms  24838  iscmet3lem3  25604  volres  25842  dvlip  26306  dvne0  26324  lhop  26329  dflog2  26881  dfrelog  26886  dvlog  26972  wilthlem2  27389  nosupbnd2lem1  28065  noinfbnd2lem1  28080  0grsubgr  29852  0pth  30709  1pthdlem1  30719  eupth2lemb  30831  ex-fpar  31056  fressupp  33274  df1stres  33290  df2ndres  33291  ffsrn  33313  resf1o  33315  fpwrelmapffs  33319  cycpmconjv  33696  evlextv  34167  sitmcl  34976  eulerpartlemn  35006  bnj1326  35649  satfv1lem  36106  divcnvlin  36477  poimirlem9  38527  zrdivrng  38867  isdrngo1  38870  cnvresrn  39260  dfsucmap2  39376  ressucdifsn  39400  disjsuc  39771  eldioph4b  43797  diophren  43799  rclexi  44600  rtrclex  44602  cnvrcl0  44610  dfrtrcl5  44614  dfrcl2  44659  relexpiidm  44689  relexp01min  44698  relexpaddss  44703  seff  45278  sblpnf  45279  radcnvrat  45283  hashnzfzclim  45291  dvresioo  46900  fourierdlem72  47157  fourierdlem80  47165  fourierdlem94  47179  fourierdlem103  47188  fourierdlem104  47189  fourierdlem113  47198  fouriersw  47210  sge0split  47388  isubgrgrim  48996  stgr0  49027  stgr1  49028  rngcidALTV  49340  ringcidALTV  49374  tposresg  49955  tposres3  49958  tposresxp  49960