Theorem reseq2d 5981

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 5976	. 2 ⊢ (𝐴 = 𝐵 → (𝐶 ↾ 𝐴) = (𝐶 ↾ 𝐵))
3	1, 2	syl 18	1 ⊢ (𝜑 → (𝐶 ↾ 𝐴) = (𝐶 ↾ 𝐵))

This proof depends on syntax axioms:   → wi 4   = wceq 1570   ↾ cres 5657

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 5171  df-xp 5661  df-res 5667

This theorem is used by:  reseq12d  5982  imadifssranOLDOLD  6216  resresdm  6247  relresfld  6296  relresfldOLD  6297  fnunres1  6673  f1orescnv  6862  fococnv2  6874  fvn0ssdmfun  7098  fnressn  7186  fnsnsplit  7212  oprssov  7614  curry1  8142  curry2  8145  dftpos2  8288  frecseq123  8328  fpr3g  8331  frrlem1  8332  frrlem4  8335  frrlem12  8343  fpr2a  8348  wfr3g  8365  dfrecs3  8408  tfrlem16  8429  tfr2ALT  8437  tfr3ALT  8438  on2recsov  8705  sbthlem4  9137  mapunen  9193  hartogslem1  9563  frr3g  9787  frr2  9791  axdc3lem2  10556  fseq1p1m1  13759  f1resfz0f1d  13954  resunimafz0  14617  hashf1lem1  14627  relexp0g  15204  relexp0  15205  relexpsucnnr  15207  dfrtrcl2  15244  bpolylem  16243  setsval  17374  idfuval  18080  idfu2nd  18081  resf1st  18098  idfusubc0  18103  idfusubc  18104  setcid  18290  catcisolem  18314  estrcid  18337  funcestrcsetclem5  18347  funcsetcestrclem5  18362  funcsetcestrclem7  18364  1stfval  18394  1stf2  18396  2ndfval  18397  2ndf2  18399  1stfcl  18400  2ndfcl  18401  curf2ndf  18450  hofcl  18462  isps  18771  cnvps  18781  isdir  18801  dirref  18804  tsrdir  18807  frmdval  19076  frmdplusg  19079  gsum2dlem2  20215  dprd2da  20288  dpjval  20302  ablfac1eulem  20318  ablfac1eu  20319  rngcval  20900  rnghmsubcsetclem1  20913  rngccat  20916  rngcid  20917  rngcifuestrc  20921  funcrngcsetc  20922  funcrngcsetcALT  20923  ringcval  20929  rhmsubcsetclem1  20942  ringccat  20945  ringcid  20946  rhmsubcrngclem1  20948  rhmsubcrngc  20950  funcringcsetc  20956  rhmsubc  20971  psrplusg  22275  opsrtoslem2  22395  mdetunilem3  22959  mdetunilem4  22960  mdetunilem9  22965  imacmp  23745  ptuncnv  24156  tgphaus  24466  tsmsres  24493  tsmsxplem1  24502  tsmsxplem2  24503  trust  24578  metreslem  24711  imasdsf1olem  24722  xmspropd  24822  mspropd  24823  imasf1oxms  24838  imasf1oms  24839  nmpropd2  24944  isngp2  24946  ngppropd  24986  tngngp2  25001  cphsscph  25602  cmspropd  25700  cmssmscld  25701  mbfres2  25996  limciun  26244  dvmptres3  26306  dvmptres2  26312  dvmptntr  26321  dvlipcn  26344  dvlip2  26345  c1liplem1  26346  dvgt0lem1  26352  lhop1lem  26363  dvcnvrelem1  26367  dvcvx  26370  ftc2ditglem  26395  wilthlem2  27426  dchrval  27591  dchrelbas2  27594  noresle  28084  nosupcbv  28089  nosupno  28090  nosupdm  28091  nosupfv  28093  nosupres  28094  nosupbnd1lem1  28095  nosupbnd1lem3  28097  nosupbnd1lem5  28099  nosupbnd1  28101  nosupbnd2  28103  noinfcbv  28104  noinfno  28105  noinfdm  28106  noinffv  28108  noinfres  28109  noinfbnd1lem3  28112  noinfbnd1lem5  28114  noinfbnd1  28116  noinfbnd2  28118  noetalem1  28128  norecov  28363  norec2ov  28373  egrsubgr  29888  pfxwlk  30296  dfpth2  30344  pthhashvtx  30345  pthdlem1  30382  eupthvdres  30866  eupth2lem3  30867  eupth2  30870  eucrct2eupth  30876  hhssablo  31895  hhssnvt  31897  hhsssh  31901  fresunsn  33291  fressupp  33352  resf1o  33392  gsummpt2d  33680  gsumpart  33694  symgcom  33714  tocycval  33739  tocycfv  33740  tocycf  33748  tocyc01  33749  cycpm2tr  33750  cycpmconjslem1  33785  cycpmconjslem2  33786  nsgqusf1o  34037  extvval  34233  extvfval  34234  extvfvcl  34238  qtophaus  34538  esumcvg  34788  eulerpartlemn  35083  sseqp1  35097  signsvtn0  35269  ftc2re  35297  reprsuc  35314  bnj1385  35532  bnj1326  35726  bnj1321  35727  bnj1442  35749  bnj1450  35750  bnj1463  35755  bnj1529  35770  cvmliftlem5  36221  cvmliftlem7  36223  cvmliftlem10  36226  cvmliftlem11  36227  cvmliftlem15  36230  cvmlift2lem11  36245  cvmlift2lem12  36246  satffunlem1lem1  36334  satffunlem2lem1  36336  eldm3  36704  funsseq  36711  finixpnum  38720  poimirlem3  38733  poimirlem4  38734  poimirlem9  38739  sdclem2  38868  prdsbnd2  38921  isdivrngo  39076  drngoi  39077  elrefsymrels2  39777  eleqvrels2  39800  dibffval  42389  hdmapffval  43075  hdmapfval  43076  eqresfnbd  43479  dvun  43603  eldiophb  43961  diophrw  43963  diophin  43976  tfsconcatrev  44542  ofoafg  44548  resisoeq45d  44613  rclexi  44807  rtrclex  44809  rtrclexi  44813  cnvrcl0  44817  dfrtrcl5  44821  dfrcl2  44866  fvmptiunrelexplb0da  44877  sblpnf  45486  fresin2  46392  limsupresuz  46918  limsupvaluz  46923  limsupvaluz2  46953  supcnvlimsup  46955  climrescn  46963  liminfresuz  46999  cncfuni  47101  dvresntr  47133  dvbdfbdioolem1  47143  itgiccshift  47195  itgperiod  47196  dirkercncflem2  47319  fourierdlem46  47367  fourierdlem48  47369  fourierdlem49  47370  fourierdlem58  47379  fourierdlem72  47393  fourierdlem74  47395  fourierdlem75  47396  fourierdlem81  47402  fourierdlem88  47409  fourierdlem89  47410  fourierdlem90  47411  fourierdlem91  47412  fourierdlem92  47413  fourierdlem103  47424  fourierdlem104  47425  fourierdlem112  47433  fouriersw  47446  voncmpl  47836  tmachlem-agreeself  48151  tmachlem-agreeprod  48152  funcoressn  48317  funressnmo  48321  f1cof1blem  48349  funfocofob  48353  funressndmafv2rn  48498  f1oresf1orab  48564  upgrimpths  49212  isubgrgrim  49232  stgrfv  49256  gpgov  49345  rngcidALTV  49576  rhmsubcALTVlem3  49585  funcringcsetcALTV2lem5  49596  ringcidALTV  49610  funcringcsetclem5ALTV  49619  itcoval  49978  itcoval0mpt  49983  itcovalendof  49986  idfu1sta  50422  idfu2nda  50424  imaidfu2  50432  idfullsubc  50482  dfswapf2  50588  oppc1stf  50615  oppc2ndf  50616  1stfpropd  50617  2ndfpropd  50618  fucofvalg  50645  fucof1  50649  fucofvalne  50652  opf2fval  50745  idfudiag1  50865  aacllem  51219