Theorem reseq2d 5611

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

Syntax hints:   → wi 4   = wceq 1637   ↾ cres 5326

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-5 2001  ax-6 2069  ax-7 2105  ax-9 2166  ax-10 2186  ax-11 2202  ax-12 2215  ax-13 2422  ax-ext 2795

This theorem depends on definitions:  df-bi 198  df-an 385  df-or 866  df-tru 1641  df-ex 1860  df-nf 1864  df-sb 2062  df-clab 2804  df-cleq 2810  df-clel 2813  df-nfc 2948  df-v 3404  df-in 3787  df-opab 4918  df-xp 5330  df-res 5336

This theorem is referenced by:  reseq12d  5612  resresdm  5854  relresfld  5890  f1orescnv  6378  fococnv2  6388  fvn0ssdmfun  6582  fnressn  6659  fnsnsplit  6685  oprssov  7043  curry1  7513  curry2  7516  dftpos2  7614  wrecseq123  7653  wfr3g  7658  wfrlem1  7659  wfrlem4  7663  wfrlem4OLD  7664  wfrlem14  7674  wfr2a  7678  dfrecs3  7715  tfrlem16  7735  tfr2ALT  7743  tfr3ALT  7744  sbthlem4  8322  mapunen  8378  hartogslem1  8696  axdc3lem2  9568  fseq1p1m1  12657  resunimafz0  13466  hashf1lem1  13476  relexp0g  14005  relexp0  14006  relexpsucnnr  14008  dfrtrcl2  14045  bpolylem  15019  setsval  16119  idfuval  16760  idfu2nd  16761  resf1st  16778  setcid  16960  catcisolem  16980  estrcid  16998  funcestrcsetclem5  17009  funcsetcestrclem5  17024  funcsetcestrclem7  17026  1stfval  17056  1stf2  17058  2ndfval  17059  2ndf2  17061  1stfcl  17062  2ndfcl  17063  curf2ndf  17112  hofcl  17124  isps  17427  cnvps  17437  isdir  17457  dirref  17460  tsrdir  17463  frmdval  17613  frmdplusg  17616  gsum2dlem2  18591  dprd2da  18663  dpjval  18677  ablfac1eulem  18693  ablfac1eu  18694  psrplusg  19610  opsrtoslem2  19713  mdetunilem3  20652  mdetunilem4  20653  mdetunilem9  20658  imacmp  21435  ptuncnv  21845  tgphaus  22154  tsmsres  22181  tsmsxplem1  22190  tsmsxplem2  22191  trust  22267  metreslem  22401  imasdsf1olem  22412  xmspropd  22512  mspropd  22513  imasf1oxms  22528  imasf1oms  22529  nmpropd2  22633  isngp2  22635  ngppropd  22675  tngngp2  22690  cphsscph  23283  cmspropd  23380  mbfres2  23649  limciun  23895  dvmptres3  23956  dvmptres2  23962  dvmptntr  23971  dvlipcn  23994  dvlip2  23995  c1liplem1  23996  dvgt0lem1  24002  lhop1lem  24013  dvcnvrelem1  24017  dvcvx  24020  ftc2ditglem  24045  wilthlem2  25032  dchrval  25196  dchrelbas2  25199  egrsubgr  26408  pthdlem1  26913  eupthvdres  27431  eupth2lem3  27432  eupth2  27435  eucrct2eupth  27441  hhssablo  28471  hhssnvt  28473  hhsssh  28477  fnunres1  29765  resf1o  29855  gsummpt2d  30129  qtophaus  30251  esumcvg  30496  eulerpartlemn  30791  sseqp1  30805  signsvtn0  30995  ftc2re  31024  reprsuc  31041  bnj1385  31248  bnj1326  31439  bnj1321  31440  bnj1442  31462  bnj1450  31463  bnj1463  31468  bnj1529  31483  cvmliftlem5  31616  cvmliftlem7  31618  cvmliftlem10  31621  cvmliftlem11  31622  cvmliftlem15  31625  cvmlift2lem11  31640  cvmlift2lem12  31641  eldm3  31995  funsseq  32010  frecseq123  32120  frr3g  32122  frrlem1  32123  frrlem4  32126  noresle  32189  nosupno  32192  nosupdm  32193  nosupfv  32195  nosupres  32196  nosupbnd1lem1  32197  nosupbnd1lem3  32199  nosupbnd1lem5  32201  nosupbnd1  32203  nosupbnd2  32205  noeta  32211  finixpnum  33726  poimirlem3  33744  poimirlem4  33745  poimirlem9  33750  sdclem2  33868  prdsbnd2  33924  isdivrngo  34079  drngoi  34080  elrefsymrels2  34647  dibffval  36939  hdmapffval  37625  hdmapfval  37626  eldiophb  37840  diophrw  37842  diophin  37856  rclexi  38440  rtrclex  38442  rtrclexi  38446  cnvrcl0  38450  dfrtrcl5  38454  dfrcl2  38484  fvmptiunrelexplb0da  38495  sblpnf  39027  fresin2  39859  limsupresuz  40433  limsupvaluz  40438  limsupvaluz2  40468  supcnvlimsup  40470  climrescn  40478  liminfresuz  40514  cncfuni  40597  dvresntr  40630  dvbdfbdioolem1  40641  itgiccshift  40693  itgperiod  40694  dirkercncflem2  40818  fourierdlem46  40866  fourierdlem48  40868  fourierdlem49  40869  fourierdlem58  40878  fourierdlem72  40892  fourierdlem74  40894  fourierdlem75  40895  fourierdlem81  40901  fourierdlem88  40908  fourierdlem89  40909  fourierdlem90  40910  fourierdlem91  40911  fourierdlem92  40912  fourierdlem103  40923  fourierdlem104  40924  fourierdlem112  40932  fouriersw  40945  voncmpl  41335  funcoressn  41679  funressnmo  41683  funressndmafv2rn  41830  f1oresf1orab  41897  idfusubc0  42451  idfusubc  42452  rngcval  42548  rnghmsubcsetclem1  42561  rngccat  42564  rngcid  42565  rngcidALTV  42577  rngcifuestrc  42583  funcrngcsetc  42584  funcrngcsetcALT  42585  ringcval  42594  rhmsubcsetclem1  42607  ringccat  42610  ringcid  42611  rhmsubcrngclem1  42613  rhmsubcrngc  42615  funcringcsetc  42621  funcringcsetcALTV2lem5  42626  ringcidALTV  42640  funcringcsetclem5ALTV  42649  rhmsubc  42676  rhmsubcALTVlem3  42692  aacllem  43136