Theorem reseq2d 5317

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

Syntax hints:   → wi 4   = wceq 1475   ↾ cres 5040

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-v 3175  df-in 3547  df-opab 4644  df-xp 5044  df-res 5050

This theorem is referenced by:  reseq12d  5318  resima2OLD  5353  relresfld  5579  f1orescnv  6065  fococnv2  6075  fvn0ssdmfun  6258  fnressn  6330  fnsnsplit  6355  oprssov  6701  curry1  7156  curry2  7159  dftpos2  7256  wrecseq123  7295  wfr3g  7300  wfrlem1  7301  wfrlem4  7305  wfrlem14  7315  wfr2a  7319  dfrecs3  7356  tfrlem16  7376  tfr2ALT  7384  tfr3ALT  7385  sbthlem4  7958  mapunen  8014  hartogslem1  8330  axdc3lem2  9156  fseq1p1m1  12283  hashf1lem1  13096  relexp0g  13610  relexp0  13611  relexpsucnnr  13613  dfrtrcl2  13650  bpolylem  14618  setsval  15720  idfuval  16359  idfu2nd  16360  resf1st  16377  setcid  16559  catcisolem  16579  estrcid  16597  funcestrcsetclem5  16607  funcsetcestrclem5  16622  funcsetcestrclem7  16624  1stfval  16654  1stf2  16656  2ndfval  16657  2ndf2  16659  1stfcl  16660  2ndfcl  16661  curf2ndf  16710  hofcl  16722  isps  17025  cnvps  17035  isdir  17055  dirref  17058  tsrdir  17061  frmdval  17211  frmdplusg  17214  gsum2dlem2  18193  dprd2da  18264  dpjval  18278  ablfac1eulem  18294  ablfac1eu  18295  psrplusg  19202  opsrtoslem2  19306  mdetunilem3  20239  mdetunilem4  20240  mdetunilem9  20245  imacmp  21010  ptuncnv  21420  tgphaus  21730  tsmsres  21757  tsmsxplem1  21766  tsmsxplem2  21767  trust  21843  metreslem  21977  imasdsf1olem  21988  xmspropd  22088  mspropd  22089  imasf1oxms  22104  imasf1oms  22105  nmpropd2  22209  isngp2  22211  ngppropd  22251  tngngp2  22266  cmspropd  22954  mbfres2  23218  limciun  23464  dvmptres3  23525  dvmptres2  23531  dvmptntr  23540  dvlipcn  23561  dvlip2  23562  c1liplem1  23563  dvgt0lem1  23569  lhop1lem  23580  dvcnvrelem1  23584  dvcvx  23587  ftc2ditglem  23612  wilthlem2  24595  dchrval  24759  dchrelbas2  24762  ausisusgraedg  25885  1pthonlem1  26119  constr2pth  26131  eupath2lem3  26506  eupath2  26507  hhssablo  27504  hhssnvt  27506  hhsssh  27510  resf1o  28893  gsummpt2d  29112  qtophaus  29231  esumcvg  29475  eulerpartlemn  29770  sseqp1  29784  signsvtn0  29973  bnj1385  30157  bnj1326  30348  bnj1321  30349  bnj1442  30371  bnj1450  30372  bnj1463  30377  bnj1529  30392  cvmliftlem5  30525  cvmliftlem7  30527  cvmliftlem10  30530  cvmliftlem11  30531  cvmliftlem15  30534  cvmlift2lem11  30549  cvmlift2lem12  30550  eldm3  30905  funsseq  30912  frr3g  31023  frrlem1  31024  frrlem4  31027  finixpnum  32564  poimirlem3  32582  poimirlem4  32583  poimirlem9  32588  sdclem2  32708  prdsbnd2  32764  isdivrngo  32919  drngoi  32920  dibffval  35447  hdmapffval  36136  hdmapfval  36137  eldiophb  36338  diophrw  36340  diophin  36354  rclexi  36941  rtrclex  36943  rtrclexi  36947  cnvrcl0  36951  dfrtrcl5  36955  dfrcl2  36985  fvmptiunrelexplb0da  36996  sblpnf  37531  fresin2  38347  cncfuni  38772  dvresntr  38806  dvbdfbdioolem1  38818  itgiccshift  38872  itgperiod  38873  dirkercncflem2  38997  fourierdlem46  39045  fourierdlem48  39047  fourierdlem49  39048  fourierdlem58  39057  fourierdlem72  39071  fourierdlem74  39073  fourierdlem75  39074  fourierdlem81  39080  fourierdlem88  39087  fourierdlem89  39088  fourierdlem90  39089  fourierdlem91  39090  fourierdlem92  39091  fourierdlem103  39102  fourierdlem104  39103  fourierdlem112  39111  fouriersw  39124  voncmpl  39511  funcoressn  39856  resresdm  40319  resunimafz0  40368  egrsubgr  40501  pthdlem1  40972  eupthvdres  41403  eupth2lem3  41404  eupth2  41407  eucrct2eupth  41413  idfusubc0  41655  idfusubc  41656  rngcval  41754  rnghmsubcsetclem1  41767  rngccat  41770  rngcid  41771  rngcidALTV  41783  rngcifuestrc  41789  funcrngcsetc  41790  funcrngcsetcALT  41791  ringcval  41800  rhmsubcsetclem1  41813  ringccat  41816  ringcid  41817  rhmsubcrngclem1  41819  rhmsubcrngc  41821  funcringcsetc  41827  funcringcsetcALTV2lem5  41832  ringcidALTV  41846  funcringcsetclem5ALTV  41855  rhmsubc  41882  rhmsubcALTVlem3  41899  aacllem  42356