Theorem ressid 17208

Description: Behavior of trivial restriction. (Contributed by Stefan O'Rear, 29-Nov-2014.)

Hypothesis

Ref	Expression
ressid.1	⊢ 𝐵 = (Base‘𝑊)

Assertion

Ref	Expression
ressid	⊢ (𝑊 ∈ 𝑋 → (𝑊 ↾s 𝐵) = 𝑊)

Proof of Theorem ressid

Step	Hyp	Ref	Expression
1		ssid 3945	. 2 ⊢ 𝐵 ⊆ 𝐵
2		ressid.1	. . 3 ⊢ 𝐵 = (Base‘𝑊)
3	2	fvexi 6849	. 2 ⊢ 𝐵 ∈ V
4		eqid 2737	. . 3 ⊢ (𝑊 ↾s 𝐵) = (𝑊 ↾s 𝐵)
5	4, 2	ressid2 17198	. 2 ⊢ ((𝐵 ⊆ 𝐵 ∧ 𝑊 ∈ 𝑋 ∧ 𝐵 ∈ V) → (𝑊 ↾s 𝐵) = 𝑊)
6	1, 3, 5	mp3an13 1455	1 ⊢ (𝑊 ∈ 𝑋 → (𝑊 ↾s 𝐵) = 𝑊)

Syntax hints:   → wi 4   = wceq 1542   ∈ wcel 2114  Vcvv 3430   ⊆ wss 3890  ‘cfv 6493  (class class class)co 7361  Basecbs 17173   ↾_s cress 17194

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2709  ax-sep 5232  ax-nul 5242  ax-pr 5371

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2540  df-eu 2570  df-clab 2716  df-cleq 2729  df-clel 2812  df-nfc 2886  df-ne 2934  df-ral 3053  df-rex 3063  df-rab 3391  df-v 3432  df-sbc 3730  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-nul 4275  df-if 4468  df-sn 4569  df-pr 4571  df-op 4575  df-uni 4852  df-br 5087  df-opab 5149  df-id 5520  df-xp 5631  df-rel 5632  df-cnv 5633  df-co 5634  df-dm 5635  df-iota 6449  df-fun 6495  df-fv 6501  df-ov 7364  df-oprab 7365  df-mpo 7366  df-ress 17195

This theorem is referenced by:  ressval3d  17210  submgmid  18668  submid  18772  subgid  19098  gaid2  19272  subrngid  20520  subrgid  20544  sdrgid  20763  rlmval2  21182  rlmsca  21188  rlmsca2  21189  pjff  21705  dsmmfi  21731  frlmip  21771  evlrhm  22092  evlsscasrng  22096  evlsvarsrng  22098  evl1sca  22312  evl1var  22314  evls1scasrng  22317  evls1varsrng  22318  pf1ind  22333  evl1gsumadd  22336  evl1varpw  22339  ressply1evl  22348  cnstrcvs  25121  cncvs  25125  rlmbn  25341  ishl2  25350  rrxprds  25369  dchrptlem2  27245  evl1fpws  33642  evlextv  33704  resssra  33749  rgmoddimOLD  33773  qusdimsum  33791  fldextid  33822  riccrng1  42983  ricdrng1  42990  evlsevl  43024  evlvvval  43025  evlvvvallem  43026  mhphf4  43050  lnmfg  43531  lmhmfgsplit  43535  pwslnmlem2  43542  simpcntrab  47319