Theorem reseq2d 5970

Description: Equality deduction for restrictions. (Contributed by Paul Chapman, 22-Jun-2011.)

Hypothesis

Ref	Expression
reseqd.1	⊢ (𝜑 → 𝐴 = 𝐵)

Assertion

Ref	Expression
reseq2d	⊢ (𝜑 → (𝐶 ↾ 𝐴) = (𝐶 ↾ 𝐵))

Proof of Theorem reseq2d

Step	Hyp	Ref	Expression
1		reseqd.1	. 2 ⊢ (𝜑 → 𝐴 = 𝐵)
2		reseq2 5965	. 2 ⊢ (𝐴 = 𝐵 → (𝐶 ↾ 𝐴) = (𝐶 ↾ 𝐵))
3	1, 2	syl 18	1 ⊢ (𝜑 → (𝐶 ↾ 𝐴) = (𝐶 ↾ 𝐵))

This proof depends on syntax axioms:   → wi 4   = 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:  reseq12d  5971  imadifssranOLD  6196  resresdm  6227  relresfld  6271  relresfldOLD  6272  fnunres1  6643  f1orescnv  6832  fococnv2  6843  fvn0ssdmfun  7066  fnressn  7154  fnsnsplit  7181  oprssov  7582  curry1  8104  curry2  8107  dftpos2  8244  frecseq123  8284  fpr3g  8287  frrlem1  8288  frrlem4  8291  frrlem12  8299  fpr2a  8304  wfr3g  8321  dfrecs3  8364  tfrlem16  8385  tfr2ALT  8393  tfr3ALT  8394  on2recsov  8661  sbthlem4  9093  mapunen  9149  hartogslem1  9520  frr3g  9744  frr2  9748  axdc3lem2  10510  fseq1p1m1  13712  f1resfz0f1d  13907  resunimafz0  14570  hashf1lem1  14580  relexp0g  15155  relexp0  15156  relexpsucnnr  15158  dfrtrcl2  15195  bpolylem  16194  setsval  17325  idfuval  18031  idfu2nd  18032  resf1st  18049  idfusubc0  18054  idfusubc  18055  setcid  18241  catcisolem  18265  estrcid  18288  funcestrcsetclem5  18298  funcsetcestrclem5  18313  funcsetcestrclem7  18315  1stfval  18345  1stf2  18347  2ndfval  18348  2ndf2  18350  1stfcl  18351  2ndfcl  18352  curf2ndf  18401  hofcl  18413  isps  18722  cnvps  18732  isdir  18752  dirref  18755  tsrdir  18758  frmdval  19027  frmdplusg  19030  gsum2dlem2  20165  dprd2da  20238  dpjval  20252  ablfac1eulem  20268  ablfac1eu  20269  rngcval  20850  rnghmsubcsetclem1  20863  rngccat  20866  rngcid  20867  rngcifuestrc  20871  funcrngcsetc  20872  funcrngcsetcALT  20873  ringcval  20879  rhmsubcsetclem1  20892  ringccat  20895  ringcid  20896  rhmsubcrngclem1  20898  rhmsubcrngc  20900  funcringcsetc  20906  rhmsubc  20921  psrplusg  22225  opsrtoslem2  22345  mdetunilem3  22909  mdetunilem4  22910  mdetunilem9  22915  imacmp  23695  ptuncnv  24106  tgphaus  24416  tsmsres  24443  tsmsxplem1  24452  tsmsxplem2  24453  trust  24528  metreslem  24661  imasdsf1olem  24672  xmspropd  24772  mspropd  24773  imasf1oxms  24788  imasf1oms  24789  nmpropd2  24894  isngp2  24896  ngppropd  24936  tngngp2  24951  cphsscph  25552  cmspropd  25650  cmssmscld  25651  mbfres2  25946  limciun  26194  dvmptres3  26256  dvmptres2  26262  dvmptntr  26271  dvlipcn  26294  dvlip2  26295  c1liplem1  26296  dvgt0lem1  26302  lhop1lem  26313  dvcnvrelem1  26317  dvcvx  26320  ftc2ditglem  26345  wilthlem2  27378  dchrval  27543  dchrelbas2  27546  noresle  28036  nosupcbv  28041  nosupno  28042  nosupdm  28043  nosupfv  28045  nosupres  28046  nosupbnd1lem1  28047  nosupbnd1lem3  28049  nosupbnd1lem5  28051  nosupbnd1  28053  nosupbnd2  28055  noinfcbv  28056  noinfno  28057  noinfdm  28058  noinffv  28060  noinfres  28061  noinfbnd1lem3  28064  noinfbnd1lem5  28066  noinfbnd1  28068  noinfbnd2  28070  noetalem1  28080  norecov  28315  norec2ov  28325  egrsubgr  29840  pfxwlk  30248  dfpth2  30296  pthhashvtx  30297  pthdlem1  30334  eupthvdres  30818  eupth2lem3  30819  eupth2  30822  eucrct2eupth  30828  hhssablo  31847  hhssnvt  31849  hhsssh  31853  fresunsn  33201  fressupp  33263  resf1o  33304  gsummpt2d  33592  gsumpart  33606  symgcom  33626  tocycval  33651  tocycfv  33652  tocycf  33660  tocyc01  33661  cycpm2tr  33662  cycpmconjslem1  33697  cycpmconjslem2  33698  nsgqusf1o  33949  extvval  34145  extvfval  34146  extvfvcl  34150  qtophaus  34450  esumcvg  34700  eulerpartlemn  34996  sseqp1  35010  signsvtn0  35182  ftc2re  35210  reprsuc  35227  bnj1385  35445  bnj1326  35639  bnj1321  35640  bnj1442  35662  bnj1450  35663  bnj1463  35668  bnj1529  35683  cvmliftlem5  36023  cvmliftlem7  36025  cvmliftlem10  36028  cvmliftlem11  36029  cvmliftlem15  36032  cvmlift2lem11  36047  cvmlift2lem12  36048  satffunlem1lem1  36136  satffunlem2lem1  36138  eldm3  36495  funsseq  36502  finixpnum  38496  poimirlem3  38509  poimirlem4  38510  poimirlem9  38515  sdclem2  38644  prdsbnd2  38697  isdivrngo  38852  drngoi  38853  elrefsymrels2  39553  eleqvrels2  39576  dibffval  42165  hdmapffval  42851  hdmapfval  42852  eqresfnbd  43254  dvun  43378  eldiophb  43721  diophrw  43723  diophin  43736  tfsconcatrev  44308  ofoafg  44314  resisoeq45d  44379  rclexi  44574  rtrclex  44576  rtrclexi  44580  cnvrcl0  44584  dfrtrcl5  44588  dfrcl2  44633  fvmptiunrelexplb0da  44644  sblpnf  45253  fresin2  46130  limsupresuz  46657  limsupvaluz  46662  limsupvaluz2  46692  supcnvlimsup  46694  climrescn  46702  liminfresuz  46738  cncfuni  46840  dvresntr  46872  dvbdfbdioolem1  46882  itgiccshift  46934  itgperiod  46935  dirkercncflem2  47058  fourierdlem46  47106  fourierdlem48  47108  fourierdlem49  47109  fourierdlem58  47118  fourierdlem72  47132  fourierdlem74  47134  fourierdlem75  47135  fourierdlem81  47141  fourierdlem88  47148  fourierdlem89  47149  fourierdlem90  47150  fourierdlem91  47151  fourierdlem92  47152  fourierdlem103  47163  fourierdlem104  47164  fourierdlem112  47172  fouriersw  47185  voncmpl  47575  tmachlem-agreeself  47890  tmachlem-agreeprod  47891  funcoressn  48056  funressnmo  48060  f1cof1blem  48088  funfocofob  48092  funressndmafv2rn  48237  f1oresf1orab  48303  upgrimpths  48951  isubgrgrim  48971  stgrfv  48995  gpgov  49084  rngcidALTV  49315  rhmsubcALTVlem3  49324  funcringcsetcALTV2lem5  49335  ringcidALTV  49349  funcringcsetclem5ALTV  49358  itcoval  49717  itcoval0mpt  49722  itcovalendof  49725  idfu1sta  50153  idfu2nda  50155  imaidfu2  50163  idfullsubc  50213  dfswapf2  50313  oppc1stf  50340  oppc2ndf  50341  1stfpropd  50342  2ndfpropd  50343  fucofvalg  50370  fucof1  50374  fucofvalne  50377  opf2fval  50457  idfudiag1  50577  aacllem  50883